mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {p₁ p₂ : P} {s : EuclideanGeometry.Sphere P},
  p₁ ∈ s → p₂ ∈ s → dist p₁ s.center = dist p₂ s.center
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.spine_injective : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) [X.IsStrictSegal] {m : ℕ} {h : m ≤ n + 1}, Function.Injective (X.spine m h)
-- Init.Core
/-- `∅` or `{}` is the empty set or empty collection.
It is supported by the `EmptyCollection` typeclass. 

Conventions for notations in identifiers:

 * The recommended spelling of `{}` in identifiers is `empty`.

 * The recommended spelling of `∅` in identifiers is `empty`. -/
EmptyCollection.emptyCollection : {α : Type u} → [self : EmptyCollection α] → α
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_fn_inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₗc[R] B}, ⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
-- Init.Data.BitVec.Basic
/-- Converts an integer to its two's complement representation as a bitvector of the given width `n`,
over- and underflowing as needed.

The underlying `Nat` is `(2^n + (i mod 2^n)) mod 2^n`. Converting the bitvector back to an `Int`
with `BitVec.toInt` results in the value `i.bmod (2^n)`.
 -/
BitVec.ofInt : (n : ℕ) → ℤ → BitVec n
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.ae_compProd_of_ae_ae : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {a : α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel (α × β) γ}
  {p : β × γ → Prop},
  MeasurableSet {x | p x} → (∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)) → ∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.optionFunLeft_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p q : MvPowerSeries (Option σ) R),
  MvPowerSeries.optionFunLeft✝ σ R (p * q) = MvPowerSeries.optionFunLeft✝ σ R p * MvPowerSeries.optionFunLeft✝ σ R q
-- Lean.Meta.Tactic.Grind.Proof
/-- Given `lhs` and `rhs` proof terms of the form `nestedDecidable p hp` and `nestedDecidable q hq`,
constructs a congruence proof for `nestedDecidable p hp ≍ nestedDecidable q hq`.
`p` and `q` are in the same equivalence class.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkNestedDecidableCongr : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  (t : CategoryTheory.Limits.ColimitCocone F) (j : J),
  CategoryTheory.CategoryStruct.comp (t.cocone.ι.app j) (CategoryTheory.Limits.colimit.isoColimitCocone t).inv =
    CategoryTheory.Limits.colimit.ι F j
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableAt.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ g x → f x ≠ 0 → DifferentiableAt ℝ (fun x => f x ^ g x) x
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_lt_iff : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : ℝ}, 0 < r → (dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r)
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.ratio.eq_1 : Std.DTreeMap.Internal.ratio = 2
-- Mathlib.Topology.Algebra.MulAction
ContinuousVAdd.mk : ∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace X],
  (Continuous fun p => p.1 +ᵥ p.2) → ContinuousVAdd M X
-- Mathlib.GroupTheory.Transfer
MonoidHom.transferSylow_domRestrict_eq_pow : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex],
  ⇑((MonoidHom.transferSylow P hP).domRestrict ↑P) = fun x => x ^ (↑P).index
-- Batteries.Data.List.Lemmas
List.dropSuffix?_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] {l p s : List α}, l.dropSuffix? s = some p ↔ ∃ s', l = p ++ s' ∧ (s' == s) = true
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the third quadrant. Let `f g : ℂ → E` be functions such that

* `f` and `g` are differentiable in the open third quadrant and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open third
  quadrant for some `A`, `B`, and `c < 2`;
* `f` is equal to `g` on the boundary of the third quadrant.

Then `f` is equal to `g` on the closed third quadrant.  -/
PhragmenLindelof.eqOn_quadrant_III : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
  DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Iio 0) →
        (∃ c < 2,
            ∃ B,
              g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
          (∀ x ≤ 0, f ↑x = g ↑x) →
            (∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)) → Set.EqOn f g {z | z.re ≤ 0 ∧ z.im ≤ 0}
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.isNat_eq_rawCast : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {a : A} {lit : ℕ},
  Mathlib.Meta.NormNum.IsNat a lit → a = (algebraMap R A) (↑lit + 0) + 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_of_mem_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C]
  (A₀ : CategoryTheory.Subobject X) (J : Type w) [inst_3 : LinearOrder J] [inst_4 : OrderBot J] [inst_5 : SuccOrder J]
  [inst_6 : WellFoundedLT J] (j : J),
  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver hG A₀ J).obj j =
    CategoryTheory.MonoOver.mk
      (transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j A₀).arrow
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] [inst : Inhabited α]
  {k : α}, m.contains k = true → m.getKey! k = k
-- Mathlib.Data.Fintype.Prod
Fintype.card_prod : ∀ (α : Type u_4) (β : Type u_5) [inst : Fintype α] [inst_1 : Fintype β],
  Fintype.card (α × β) = Fintype.card α * Fintype.card β
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_filterMap : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : Std.Internal.Do.WPMonad n Pred EPred]
  [inst_6 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ}
  {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b =>
          match f b with
          | some c => g d c
          | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.Iter.foldM g init (Std.Iter.filterMap f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instOrderTop.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass.instOrderTop = { top := ArchimedeanClass.mk 0, le_top := ⋯ }
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.setSimpParams : Lean.TSyntax `tactic → Array Lean.Syntax → Lean.TSyntax `tactic
-- Init.Data.String.Hashable
String.instHashableRaw : Hashable String.Pos.Raw
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The functor `hoFunctor : SSet ⥤ Cat` preserves finite products of simplicial sets.  -/
CategoryTheory.hoFunctor.preservesFiniteProducts : CategoryTheory.Limits.PreservesFiniteProducts SSet.hoFunctor
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.prod_eval : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β₁ : Type u_7} {β₂ : Type u_8} [inst_1 : TopologicalSpace β₁]
  [inst_2 : TopologicalSpace β₂] (f : C(α, β₁)) (g : C(α, β₂)) (a : α), (f.prodMk g) a = (f a, g a)
-- Mathlib.LinearAlgebra.Complex.Module
/-- The identity and the complex conjugation are the only two `ℝ`-algebra homomorphisms of `ℂ`.  -/
Complex.real_algHom_eq_id_or_conj : ∀ (f : ℂ →ₐ[ℝ] ℂ), f = AlgHom.id ℝ ℂ ∨ f = ↑Complex.conjAe
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.IsColimit.homIso_symm_apply : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C)
  (h :
    { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }),
  (CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z).symm h =
    ↑(CategoryTheory.Limits.Cotrident.IsColimit.desc' ht ↑h ⋯)
-- Init.WF
/-- Case analysis based on strong induction for the natural numbers.
 -/
Nat.caseStrongRecOn : {motive : ℕ → Sort u} → (a : ℕ) → motive 0 → ((n : ℕ) → ((m : ℕ) → m ≤ n → motive m) → motive n.succ) → motive a
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.prod : ∀ {α : Type u_2} {β : Type u_3} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] {t : Set β},
  CountableInfClosed s → CountableInfClosed t → CountableInfClosed (s ×ˢ t)
-- Mathlib.Combinatorics.KatonaCircle
/-- The set of numberings of which `s` is a prefix.  -/
Numbering.prefixed : {X : Type u_1} → [inst : Fintype X] → [DecidableEq X] → Finset X → Finset (Numbering X)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_algEquivOfAssociated : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : Associated f g), ⇑(AdjoinRoot.algEquivOfAssociated R f g hfg) = ⇑(AdjoinRoot.algHomOfDvd R f g ⋯)
-- Mathlib.Geometry.Manifold.Immersion
/-- Prefer using `IsImmersionAtOfComplement.contMDiffAt` instead  -/
Manifold.IsImmersionAtOfComplement.contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), ContMDiffOn I J n f h.domChart.source
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.coe_bot : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜], ↑⊥ = 0
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.NamedLinter.mk.sizeOf_spec : ∀ (toLinter : Batteries.Tactic.Lint.Linter) (name declName : Lean.Name),
  sizeOf { toLinter := toLinter, name := name, declName := declName } =
    1 + sizeOf toLinter + sizeOf name + sizeOf declName
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.functorExt_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1}
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} (base : F.obj none ≅ G.obj none)
  (comp : (i : ι) → F.obj (some i) ≅ G.obj (some i))
  (w :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) base.hom =
          CategoryTheory.CategoryStruct.comp (comp i).hom (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)))
      CategoryTheory.Limits.WidePullbackShape.functorExt._auto_1)
  (X : CategoryTheory.Limits.WidePullbackShape ι),
  (CategoryTheory.Limits.WidePullbackShape.functorExt base comp w).inv.app X =
    (match X with
      | none => base
      | some i => comp i).inv
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.mapRange_finsuppAntidiag_subset : ∀ {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ]
  [inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] [inst_4 : AddCommMonoid μ']
  [inst_5 : Finset.HasAntidiagonal μ'] [inst_6 : DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ},
  Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)
-- Mathlib.CategoryTheory.IsConnected
/-- `j₁` and `j₂` are related by `Zigzag` if there is a chain of
morphisms from `j₁` to `j₂`, with backward morphisms allowed.
 -/
CategoryTheory.Zigzag : {J : Type u₁} → [CategoryTheory.Category.{v₁, u₁} J] → J → J → Prop
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_e_f : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → ⁅e, f⁆ = h
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.indep_maximal : ∀ {α : Type u_2} (self : IndepMatroid α), ∀ X ⊆ self.E, Matroid.ExistsMaximalSubsetProperty self.Indep X
-- Std.Time.Zoned
/-- Converts a `PlainDate` to a `DateTime`.
 -/
Std.Time.DateTime.ofLocalDate : Std.Time.PlainDate → Std.Time.TimeZone.ZoneRules → Std.Time.DateTime
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.equivSubtype_apply_coe : ∀ (R : Type u_1) [inst : CommSemiring R] (I : MaximalSpectrum R), ↑((MaximalSpectrum.equivSubtype R) I) = I.asIdeal
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_mul_right_eq_mul_conj : ∀ {G : Type u_1} [inst : Group G] (a b c : G), ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryLT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryLT! t₁ k = Std.DTreeMap.Raw.Const.getEntryLT! t₂ k
-- Init.Tactics
/-- `get_elem_tactic` is the tactic automatically called by the notation `arr[i]`
to prove any side conditions that arise when constructing the term
(e.g. the index is in bounds of the array). It just delegates to
`get_elem_tactic_extensible` and gives a diagnostic error message otherwise;
users are encouraged to extend `get_elem_tactic_extensible` instead of this tactic.
 -/
tacticGet_elem_tactic : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.isIso_inr_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Epi f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inr f f)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.equivLike_inv_eq_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ* N), EquivLike.inv f = ⇑f.symm
-- Std.Http.Data.Headers
Std.Http.instReprHeaders : Repr Std.Http.Headers
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.ofZeros_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
  (hg₂ : S₂.g = 0),
  (CategoryTheory.ShortComplex.HomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).left =
    CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.congr_fun : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f g : M ≃+ N}, f = g → ∀ (x : M), f x = g x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The morphism of exterior algebras induced by a linear map.  -/
ExteriorAlgebra.map : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type u4} →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] → (M →ₗ[R] N) → ExteriorAlgebra R M →ₐ[R] ExteriorAlgebra R N
-- Lean.Elab.InfoTree.Types
Lean.Elab.UserWidgetInfo.mk.injEq : ∀ (toWidgetInstance : Lean.Widget.WidgetInstance) (stx : Lean.Syntax) (toWidgetInstance_1 : Lean.Widget.WidgetInstance)
  (stx_1 : Lean.Syntax),
  ({ toWidgetInstance := toWidgetInstance, stx := stx } = { toWidgetInstance := toWidgetInstance_1, stx := stx_1 }) =
    (toWidgetInstance = toWidgetInstance_1 ∧ stx = stx_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback v : β k}, (m.insert k v).getD k fallback = v
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.vecMul_swap_apply : ∀ {R : Type u_1} {n : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (a : n → R),
  Matrix.vecMul a (Matrix.swap R i j) i = a j
-- Mathlib.Order.Disjoint
Disjoint.sup_left : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
  Disjoint a c → Disjoint b c → Disjoint (a ⊔ b) c
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {X : Type u_6} [inst_5 : TopologicalSpace X] {f : X → E →L[𝕜] F} {g : X → E} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => (f x) (g x)) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.any_eq_true' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulBEq α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).any p = true ↔ ∃ a, ∃ (h : m.contains a = true), p a (Std.DHashMap.Internal.Raw₀.Const.get m a h) = true)
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.semilatticeSup : {α : Type u_1} → [inst : SemilatticeSup α] → {a : α} → SemilatticeSup { x // a ≤ x }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommSemiring.mk.sizeOf_spec : ∀ (toSemiring : Lean.Meta.Grind.Arith.CommRing.Semiring) (ringId : ℕ) (commSemiringInst : Lean.Expr)
  (addRightCancelInst? : Option (Option Lean.Expr)) (toQFn? : Option Lean.Expr),
  sizeOf
      { toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
        addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? } =
    1 + sizeOf toSemiring + sizeOf ringId + sizeOf commSemiringInst + sizeOf addRightCancelInst? + sizeOf toQFn?
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_mul_cancel_right_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix m n α) [Invertible A], B * A⁻¹ * A = B
-- Mathlib.CategoryTheory.Sites.Spaces
CategoryTheory.GrothendieckTopology.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sieves sieves_1 : (X : C) → Set (CategoryTheory.Sieve X))
  (e_sieves : sieves = sieves_1) (top_mem' : ∀ (X : C), ⊤ ∈ sieves X)
  (pullback_stable' :
    ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y)
  (transitive' :
    ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ sieves X →
        ∀ (R : CategoryTheory.Sieve X),
          (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X),
  { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' } =
    { sieves := sieves_1, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.ext : ∀ {D : Type u_1} {Q : Type u_2} {x y : D ≀ᵣ Q}, x.left = y.left → x.right = y.right → x = y
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_3.eq_3 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : (n : ℕ) → motive n.succ.succ.succ.succ),
  (match 2 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | n.succ.succ.succ.succ => h_5 n) =
    h_3 ()
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G'] [inst_6 : NormedSpace ℝ G'] (T : Set α → G' →L[ℝ] G''),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ (f : MeasureTheory.SimpleFunc α G'),
      0 ≤ f → MeasureTheory.Integrable (⇑f) μ → 0 ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Mathlib.Topology.Separation.Basic
/-- A topological space is called a *preregular* (a.k.a. R₁) space,
if any two topologically distinguishable points have disjoint neighbourhoods.  -/
R1Space : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G),
  (CategoryTheory.NatIso.unop α).inv = CategoryTheory.NatTrans.unop α.inv
-- Mathlib.Data.Int.Fib.Basic
Int.fib_two_mul_add_two : ∀ (n : ℤ), Int.fib (2 * n + 2) = Int.fib (n + 1) * (2 * Int.fib n + Int.fib (n + 1))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filterMap' : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α]
  {f : (a : α) × β a → Option ((a : α) × γ a)},
  (∀ (p : (a : α) × β a), Option.all (fun x => x.fst == p.fst) (f p) = true) →
    ∀ {l : List ((a : α) × β a)} {k : α},
      Std.Internal.List.DistinctKeys l →
        Std.Internal.List.getEntry? k (List.filterMap f l) = (Std.Internal.List.getEntry? k l).bind f