mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (ev : (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T)))
  (ev_precomp :
    autoParam
      (∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j),
        (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (ev i j a b) =
          ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b))
      CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp._autoParam)
  (ev_1 : (i j : I) → ⦃T : C⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj (Opposite.op T)))
  (ev_precomp_1 :
    autoParam
      (∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j),
        (CategoryTheory.ConcreteCategory.hom (G.map φ.op)) (ev_1 i j a b) =
          ev_1 i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b))
      CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp._autoParam),
  ({ ev := ev, ev_precomp := ev_precomp } = { ev := ev_1, ev_precomp := ev_precomp_1 }) = (ev = ev_1)
-- Init.Meta.Defs
Array.mapSepElems : Array Lean.Syntax → (Lean.Syntax → Lean.Syntax) → Array Lean.Syntax
-- Mathlib.Algebra.Free
FreeAddSemigroup.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), FreeAddSemigroup.map f = FreeAddSemigroup.lift (FreeAddSemigroup.of ∘ f)
-- Mathlib.CategoryTheory.Action.Basic
/-- `Functor.mapAction` preserves isomorphisms of functors.  -/
CategoryTheory.Functor.mapActionCongr : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} W] →
        (G : Type u_3) →
          [inst_2 : Monoid G] → {F F' : CategoryTheory.Functor V W} → (F ≅ F') → (F.mapAction G ≅ F'.mapAction G)
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableDiv : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Div α] [DiscreteMeasurableSpace α], MeasurableDiv α
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.continuousAt_of_dominated : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_8}
  [inst_6 : TopologicalSpace Y] [FirstCountableTopology Y] {F_1 : Y → X → E} {x₀ : Y} {bound : X → ℝ},
  (∀ᶠ (x : Y) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F_1 x) μ.variation) →
    (∀ᶠ (x : Y) in nhds x₀, ∀ᵐ (a : X) ∂μ.variation, ‖F_1 x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ.variation →
        (∀ᵐ (a : X) ∂μ.variation, ContinuousAt (fun x => F_1 x a) x₀) →
          ContinuousAt (fun x => ∫ᵛ (a : X), F_1 x a ∂[B; μ]) x₀
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᴬ[R] Q), ⇑f.contLinear = ⇑(↑f).linear
-- Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
PiTensorProduct.ofDirectSumEquiv_tprod_lof : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : (i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  PiTensorProduct.ofDirectSumEquiv ((PiTensorProduct.tprod R) fun i => (DirectSum.lof R (κ i) (M i) (p i)) (x i)) =
    (DirectSum.lof R ((i : ι) → κ i) (fun i => PiTensorProduct R fun i_1 => M i_1 (i i_1)) p)
      ((PiTensorProduct.tprod R) fun i => x i)
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.coeff_isUnit : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → ∀ {k : ℕ}, k ∈ p.support → IsUnit (p.coeff k)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] [inst_2 : Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).get!
-- Lean.Compiler.IR.Basic
Lean.IR.instToStringVarId : ToString Lean.IR.VarId
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_single_add_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M},
  f₁ ≠ f₂ → g₁ ≠ 0 → g₂ ≠ 0 → ((fun₀ | f₁ => g₁) + fun₀ | f₂ => g₂).support = {f₁, f₂}
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f f_1 : M →ₗ[R] M') (e_f : f = f_1)
  [inst_5 : IsLocalizedModule S f],
  IsLocalizedModule.fromLocalizedModule S f = IsLocalizedModule.fromLocalizedModule S f_1
-- Aesop.Tree.AddRapp
Aesop.addRappUnsafe : Aesop.AddRapp → Aesop.TreeM Aesop.RappRef
-- Init.Internal.Order.Basic
Lean.Order.coind_monotone_or : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ f₂ : α → Prop),
  Lean.Order.monotone f₁ → Lean.Order.monotone f₂ → Lean.Order.monotone fun x => f₁ x ∨ f₂ x
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_def`. -/
NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] {x : K},
  (NumberField.HeightOneSpectrum.adicAbv K v) x =
    ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))
-- Mathlib.RingTheory.OreLocalization.Basic
_private.Mathlib.RingTheory.OreLocalization.Basic.0.OreLocalization.add''.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (r₁ : X) (s₁ : ↥S) (r₂ : X) (s₂ : ↥S),
  OreLocalization.add''✝ r₁ s₁ r₂ s₂ =
    (OreLocalization.oreDenom (↑s₁) s₂ • r₁ + OreLocalization.oreNum (↑s₁) s₂ • r₂) /ₒ
      (OreLocalization.oreDenom (↑s₁) s₂ * s₁)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- **Alias** of the forward direction of `mdifferentiableWithinAt_insert`. -/
MDifferentiableWithinAt.of_insert : ∀ {𝕜 : 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 : M → M'} {x : M} {s : Set M}
  {y : M}, MDiffAt[insert y s] f x → MDiffAt[s] f x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (idx : ℕ) (hidx : idx < curr)
  (hfoo :
    aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).vec.get idx ⋯ =
    (s.get idx hidx).cast hfoo
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.applyEqLemma : (Lean.Expr → Nat.EqResult✝) → Lean.Name → Array Lean.Expr → Lean.Meta.SimpM (Option Nat.EqResult✝)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] (w : m → α) (v : n → α),
  Matrix.vecMulVec w v = Matrix.of fun x y => w x * v y
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((fun₀ | (1, h) => (A.ρ g⁻¹) a) - fun₀ | (g, 1) => a) ∈ groupHomology.boundaries₂ A
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The solutions in a module `N` to the linear equations
given by `exteriorPower.relations R ι M` identify to alternating maps to `N`.  -/
exteriorPower.presentation.relationsSolutionEquiv : {R : Type u} →
  [inst : CommRing R] →
    {N : Type u_2} →
      [inst_1 : AddCommGroup N] →
        [inst_2 : Module R N] →
          {ι : Type u_4} →
            [inst_3 : DecidableEq ι] →
              {M : Type u_5} →
                [inst_4 : AddCommGroup M] →
                  [inst_5 : Module R M] → (exteriorPower.presentation.relations R ι M).Solution N ≃ M [⋀^ι]→ₗ[R] N
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCocone` commutes with `whisker`  -/
CategoryTheory.Functor.mapCoconeWhisker : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                (H : CategoryTheory.Functor C D) →
                  {F : CategoryTheory.Functor J C} →
                    {E : CategoryTheory.Functor K J} →
                      {c : CategoryTheory.Limits.Cocone F} →
                        H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c) ≅
                          CategoryTheory.Limits.Cocone.whisker E (H.mapCocone c)
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.next : ∀ {l : List Char} {c : Char} {r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l (c :: r) it → String.Legacy.Iterator.ValidFor (c :: l) r it.next
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.instInhabitedScopedEntries.default : {β : Type} → Lean.ScopedEnvExtension.ScopedEntries β
-- Lean.Meta.Match.Match
/-- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
It also returns an Boolean that indicates whether a new matcher function was added to the environment or not.  -/
Lean.Meta.Match.mkMatcherAuxDefinition : Lean.Name → Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit))
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `simp`-normal form of `invFun_eq_symm`.  -/
OrderMonoidIso.coe_toEquiv_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), ⇑(↑f).symm = ⇑f.symm
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.instHasLiftingPropertyMap_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} {A B : J → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct A] [inst_2 : CategoryTheory.Limits.HasCoproduct B]
  (f : (j : J) → A j ⟶ B j) {X Y : C} (p : X ⟶ Y) [∀ (j : J), CategoryTheory.HasLiftingProperty (f j) p],
  CategoryTheory.HasLiftingProperty (CategoryTheory.Limits.Sigma.map f) p
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj),
  (Bundle.Pretrivialization.codExtend hs nonempty e).baseSet = Subtype.val '' e.baseSet
-- Mathlib.Algebra.Module.PUnit
PUnit.instSMulCommClass : ∀ {R : Type u_1} {S : Type u_2}, SMulCommClass R S PUnit.{u_3 + 1}
-- Init.Data.List.Lemmas
List.not_mem_append : ∀ {α : Type u_1} {a : α} {s t : List α}, a ∉ s → a ∉ t → a ∉ s ++ t
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.zero_sub_add : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r : R} {s t : ↥S},
  0 -ₒ t + (r -ₒ s) = r -ₒ (s + t)
-- Init.Data.Int.Order
Int.lt_add_of_neg_lt_sub_right : ∀ {a b c : ℤ}, -b < a - c → c < a + b
-- Mathlib.Algebra.Group.Defs
mul_ne_mul_left : ∀ {G : Type u_1} [inst : Mul G] [IsRightCancelMul G] (a : G) {b c : G}, b * a ≠ c * a ↔ b ≠ c
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.below : {M : Type u_1} →
  [inst : Mul M] →
    {r : M → M → Prop} → {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} → {a a_1 : M} → ConGen.Rel r a a_1 → Prop
-- Mathlib.Tactic.ComputeDegree
/-- **Alias** of `Mathlib.Tactic.ComputeDegree.tryRfl`.

---

`tryRfl mvs` takes as input a list of `MVarId`s, scans them partitioning them into two
lists: the goals containing some metavariables and the goals not containing any metavariable.

If a goal containing a metavariable has the form `?_ = x`, `x = ?_`, where `?_` is a metavariable
and `x` is an expression that does not involve metavariables, then it closes this goal using `rfl`,
effectively assigning the metavariable to `x`.

If a goal does not contain metavariables, it tries `rfl` on it.

It returns the list of `MVarId`s, beginning with the ones that initially involved (`Expr`)
metavariables followed by the rest.
 -/
Mathlib.Tactic.ComputeDegree.try_rfl : List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Group.Action.Opposite
IsScalarTower.opposite_mid : ∀ {M : Type u_5} {N : Type u_6} [inst : Mul N] [inst_1 : SMul M N] [SMulCommClass M N N], IsScalarTower M Nᵐᵒᵖ N
-- Mathlib.Analysis.Calculus.VectorField
ContDiffOn.lieBracketWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {m n : WithTop ℕ∞},
  ContDiffOn 𝕜 n V s →
    ContDiffOn 𝕜 n W s → UniqueDiffOn 𝕜 s → m + 1 ≤ n → ContDiffOn 𝕜 m (VectorField.lieBracketWithin 𝕜 V W s) s
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.smul_mk_mk : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (g h : G) (i : ιₚ),
  g • { index := i, groupElts := ⟦h⟧ } = { index := i, groupElts := ↑(g * h) }
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instFaithfulUliftFunctor : ∀ (R : Type u) [inst : Ring R], (ModuleCat.uliftFunctor.{v', v, u} R).Faithful
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.foldl_eq_foldl_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {α_1 : Type u_2} {f : α_1 → α → α_1} {init : α_1} {t : RBTree.RBSet α cmp},
  RBTree.RBSet.foldl f init t = List.foldl f init t.toList
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_neg_one : (-1).sqrt = Complex.I
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.IsLocal.le_jacobson : ∀ {R : Type u} [inst : CommRing R] {I J : Ideal R}, I.IsLocal → I ≤ J → J ≠ ⊤ → J ≤ I.jacobson
-- Lean.Compiler.ModPkgExt
Lean.ModuleEnvExtension.getStateByIdx? : {σ : Type} → [Inhabited σ] → Lean.ModuleEnvExtension σ → Lean.Environment → Lean.ModuleIdx → Option σ
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_injective : ∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α], Function.Injective Int.cast
-- Mathlib.GroupTheory.Subgroup.Simple
/-- Any normal subgroup is either `⊥` or `⊤`  -/
IsSimpleGroup.eq_bot_or_eq_top_of_normal : ∀ {G : Type u_1} {inst : Group G} [self : IsSimpleGroup G] (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_sumCoords_eq_finsum : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), ⇑b.sumCoords = fun m => ∑ᶠ (i : ι), (b.coord i) m
-- Plausible.Shrinkable
Plausible.UInt64.shrinkable : Plausible.Shrinkable UInt64
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom
      (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃ =
    -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ
-- Mathlib.Data.Set.Lattice
Set.iUnion_plift_up : ∀ {α : Type u_1} {ι : Sort u_5} (f : PLift ι → Set α), ⋃ i, f { down := i } = ⋃ i, f i
-- Std.Do.Triple.SpecLemmas
MonadReader.read.eq_1 : ∀ {ρ : Type u} (m : Type u → Type v) [self : MonadReader ρ m], read = self.1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.beq_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp]
  {m₃ m₄ : Std.TreeSet.Raw α cmp}, m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.range_IicExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β),
  Set.range (Set.IicExtend f) = Set.range f
-- Mathlib.Topology.Compactness.Compact
IsCompact.union : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsCompact t → IsCompact (s ∪ t)
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_add_left_of_le' : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ᶠ (x : α) in l, C ≤ f x) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.PresheafHom.isAmalgamation_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X : C} (S : CategoryTheory.Sieve X)
  (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows),
  x.Compatible →
    ∀ (y : (CategoryTheory.presheafHom F G).obj (Opposite.op X)),
      x.IsAmalgamation y ↔
        ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
          y.app (Opposite.op (CategoryTheory.Over.mk g)) =
            (x g hg).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Y)))
-- Mathlib.Data.Rel
SetRel.inter_cod_subset_image_preimage : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β}, t ∩ R.cod ⊆ R.image (R.preimage t)
-- Mathlib.Algebra.Quandle
Quandle.dihedralAct.eq_1 : ∀ (n : ℕ) (a b : ZMod n), Quandle.dihedralAct n a b = 2 * a - b
-- Mathlib.SetTheory.Lists
Lists'.toList_cons : ∀ {α : Type u_1} (a : Lists α) (l : Lists' α true), (Lists'.cons a l).toList = a :: l.toList
-- Mathlib.Analysis.Normed.Operator.Basic
SemilinearMapClass.bound_of_shell_semi_normed : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) {ε C : ℝ},
  0 < ε →
    ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) → ∀ {x : E}, ‖x‖ ≠ 0 → ‖f x‖ ≤ C * ‖x‖
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalOrder : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Analytic.WithLp
PiLp.analyticOn_toLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] {E : ι → Type u_3} [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (p : ENNReal)
  [inst_4 : Fact (1 ≤ p)] (s : Set ((i : ι) → E i)), AnalyticOn 𝕜 (WithLp.toLp p) s
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.coe_comp_botHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedOrderHom β γ)
  (g : BoundedOrderHom α β), ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → UpperSet α), (⨆ i, f i).compl = ⨆ i, (f i).compl
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.Functor.isCardinalAccessible_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} K]
  {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} (c : CategoryTheory.Limits.Cone F)
  (hc : CategoryTheory.Limits.IsLimit c) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasLimitsOfShape K (Type w')],
  HasCardinalLT (CategoryTheory.Arrow K) κ →
    ∀ [∀ (k : K), (F.obj k).IsCardinalAccessible κ], c.pt.IsCardinalAccessible κ
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_neg_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeAddGroup α}, (-x).norm = x.norm
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.continuous_ofCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  Continuous NumberField.InfinitePlace.Completion.ofCompletion
-- Mathlib.Data.Set.Lattice
Set.biInter_le : ∀ {α : Type u_1} {ι : Type u_12} [inst : PartialOrder ι] (s : ι → Set α) (i : ι),
  ⋂ j, ⋂ (_ : j ≤ i), s j = (⋂ j, ⋂ (_ : j < i), s j) ∩ s i
-- Lean.EnvExtension
/-- Get the list of values used to update the state of the given
`SimplePersistentEnvExtension` in the current file.  -/
Lean.SimplePersistentEnvExtension.getEntries : {α σ : Type} →
  [Inhabited σ] →
    (ext : Lean.SimplePersistentEnvExtension α σ) →
      Lean.Environment → optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode → List α
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_apply_eq_zero_iff : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : MulZeroOneClass R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a : α} {e : Sym2 α} [Nontrivial R],
  SimpleGraph.incMatrix R G a e = 0 ↔ e ∉ G.incidenceSet a
-- Init.Data.Option.Array
Option.size_toArray_choice_eq_one : ∀ {α : Type u_1} [Nonempty α], (Option.choice α).toArray.size = 1
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.mk.sizeOf_spec : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {F : Ctop.Realizer α} {f : β → Set α} [inst_1 : SizeOf α]
  [inst_2 : SizeOf β] [inst_3 : (a : β) → (a_1 : α) → SizeOf (f a a_1)] (bas : (a : α) → { s // a ∈ F.F.f s })
  (sets : (x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(bas x)).Nonempty}), sizeOf { bas := bas, sets := sets } = 1
-- Mathlib.Algebra.Order.Floor.Ring
Mathlib.Meta.Positivity.nat_ceil_pos : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a : α}, 0 < a → 0 < ⌈a⌉₊
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.one_le_scalingConstantOf : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] (K : ℝ), 1 ≤ IsUnifLocDoublingMeasure.scalingConstantOf μ K
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.instInhabited : (Δ : SimplexCategoryᵒᵖ) → Inhabited (CategoryTheory.SimplicialObject.Splitting.IndexSet Δ)