mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Card
Set.Infinite.exists_subset_ncard_eq : ∀ {α : Type u_1} {s : Set α}, s.Infinite → ∀ (k : ℕ), ∃ t ⊆ s, t.Finite ∧ t.ncard = k
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `Finset.card_pow_mono` for a version that works for the empty set.  -/
Finset.Nonempty.card_pow_mono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CancelMonoid α] {s : Finset α},
  s.Nonempty → Monotone fun n => (s ^ n).card
-- Mathlib.Combinatorics.Quiver.Path
/-- A path witnesses that its target is reachable from its source.  -/
Quiver.Path.reachable : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), Quiver.Reachable a b
-- Mathlib.Analysis.Normed.Group.Basic
zero_lt_one_add_norm_sq : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), 0 < 1 + ‖x‖ ^ 2
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).get? k = Option.map f (m.get? k)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheaf.ι_evalHom_assoc : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (N : Type u)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
  {Z : Type u} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).obj) U)
      (CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I N x) h) =
    CategoryTheory.CategoryStruct.comp (TypeCat.ofHom (smoothSheaf.evalAt IM I N x (Opposite.unop U))) h
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_of_isCharThreeJNeZeroNF_of_char_three : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsCharThreeJNeZeroNF] [CharP F 3],
  W.j = -W.a₂ ^ 3 / W.a₆
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The unbundled `directLimit` of modules is a colimit
in the sense of `CategoryTheory`.  -/
ModuleCat.directLimitIsColimit : {R : Type u} →
  [inst : Ring R] →
    {ι : Type v} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Preorder ι] →
          (G : ι → Type v) →
            [inst_3 : (i : ι) → AddCommGroup (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  [inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)] →
                    CategoryTheory.Limits.IsColimit (ModuleCat.directLimitCocone G f)
-- Init.Data.Nat.Div.Basic
Nat.div.inductionOn.eq_def : ∀ {motive : ℕ → ℕ → Sort u} (x y : ℕ) (ind : (x y : ℕ) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
  (base : (x y : ℕ) → ¬(0 < y ∧ y ≤ x) → motive x y),
  Nat.div.inductionOn x y ind base =
    if h : 0 < y ∧ y ≤ x then ind x y h (Nat.div.inductionOn (x - y) y ind base) else base x y h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {he : Std.DTreeMap.Internal.Impl.contains t.minKey! t = true}, t.getKey t.minKey! he = t.minKey!
-- Mathlib.Data.Finsupp.Option
Finsupp.embDomain_some_none : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M), (Finsupp.embDomain Function.Embedding.some f) none = 0
-- Mathlib.Topology.ContinuousMap.SecondCountableSpace
ContinuousMap.compactOpen_eq_generateFrom : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set (Set X)}
  {T : Set (Set Y)},
  (∀ K ∈ S, IsCompact K) →
    TopologicalSpace.IsTopologicalBasis T →
      (∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) →
        ContinuousMap.compactOpen =
          TopologicalSpace.generateFrom
            (Set.image2 (fun K t => {f | Set.MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T})
-- Mathlib.Data.Finset.Defs
Finset.pairwise_subtype_iff_pairwise_finset' : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} (r : β → β → Prop) (f : α → β),
  Pairwise (Function.onFun r fun x => f ↑x) ↔ (↑s).Pairwise (Function.onFun r f)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_congr : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
  f =ᵐ[μ] g → MeasureTheory.MemLp.toLp f hf = MeasureTheory.MemLp.toLp g hg
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.compEquiv_symm_zero : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ)
  (x : TensorProduct S T P.toExtension.CotangentSpace),
  (Algebra.Generators.CotangentSpace.compEquiv Q P).symm (0, x) =
    (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) x
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density is defined as the infimum of $|A ∩ {1, ..., n}| / n$ as n ranges over
the positive naturals.  -/
schnirelmannDensity : (A : Set ℕ) → [DecidablePred fun x => x ∈ A] → ℝ
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.inclCompMap_inv_app : ∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I)
  (j : J) (X : C (g j)), (CategoryTheory.Sigma.inclCompMap C g j).inv.app X = CategoryTheory.CategoryStruct.id ⟨g j, X⟩
-- Init.Data.Slice.Array.Iterator
/-- Allocates a new array that contains the contents of the subarray.
 -/
Subarray.copy : {α : Type u} → Subarray α → Array α
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] (i : 𝒰.I₀),
  𝒰.functorOfLocallyDirected.obj i = 𝒰.X i
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState.push : Lean.Elab.Command.AccLevelState✝ → Lean.Level → ℤ → Lean.Elab.Command.AccLevelState✝
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (q : α → PMF β) (f : β → γ),
  PMF.map f (p.bind q) = p.bind fun a => PMF.map f (q a)
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toEquiv_reindexLinearEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n'),
  ↑(Matrix.reindexLinearEquiv R A eₘ eₙ) = Matrix.reindex eₘ eₙ
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_add_le_add_one_pow : ∀ (n k : ℕ), (n + k).choose k ≤ (n + 1) ^ k
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.eq_2 : ∀ {β : Type u_3} {γ : Type u_1} {init : γ} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (out : β)
  (motive : Subtype (PlausibleForInStep out init) → Sort u_2) (c : γ)
  (property : PlausibleForInStep out init (ForInStep.done c))
  (h_1 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩)
  (h_2 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩),
  (match ⟨ForInStep.done c, property⟩ with
    | ⟨ForInStep.yield c, property⟩ => h_1 c property
    | ⟨ForInStep.done c, property⟩ => h_2 c property) =
    h_2 c property
-- Mathlib.Data.Finset.Dedup
List.toFinset.ext_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : List α}, a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instSMulMemClass : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  SMulMemClass (IntermediateField K L) K L
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalCommSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalCommSemiring R] → [IsTopologicalSemiring R] → NonUnitalCommSemiring (SeparationQuotient R)
-- Mathlib.LinearAlgebra.LinearPMap
/-- `E →ₗ.[R] F` is the notation for `E →ₛₗ.[RingHom.id R] F`.  -/
«term_→ₗ.[_]_» : Lean.TrailingParserDescr
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.ext_iff : ∀ {α : Type u} {x y : Std.PRange.UpwardEnumerable α},
  x = y ↔ Std.PRange.succ? = Std.PRange.succ? ∧ Std.PRange.succMany? = Std.PRange.succMany?
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_iso_hom_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).iso.hom.app X_1 =
    S.iso.hom.app (U.obj X_1)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthInf_comp_le : ∀ {u : ℕ → EReal} {v : ℕ → ℕ},
  Monotone u →
    (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ 0 →
      (LinearGrowth.linearGrowthSup fun n => ↑(v n)) ≠ ⊤ →
        LinearGrowth.linearGrowthInf (u ∘ v) ≤
          (LinearGrowth.linearGrowthSup fun n => ↑(v n)) * LinearGrowth.linearGrowthInf u
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.macroInline : Lean.Compiler.InlineAttributeKind
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_add_right : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a : α),
  UniformContinuous fun b => b + a
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α}
  {b : β a}, t.WF → (t.insert a b).WF
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.comap_iInf : ∀ {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ι → UniformSpace γ} {f : α → γ},
  UniformSpace.comap f (⨅ i, u i) = ⨅ i, UniformSpace.comap f (u i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {ρ : Type u_1}
  [inst_1 : ForIn Id ρ ((a : α) × β a)] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (l l_1 : ρ), l = l_1 → t.insertMany l = t_1.insertMany l_1
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
/-- For `0 < n`, the inclusion functor from the `n`-truncated simplex category to the untruncated
simplex category is initial.  -/
SimplexCategory.Truncated.initial_inclusion : ∀ {n : ℕ} [NeZero n], (SimplexCategory.Truncated.inclusion n).Initial
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.comp_sumElim : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L')
  {L3 : FirstOrder.Language} (θ : L' →ᴸ L3), θ.comp (ϕ.sumElim ψ) = (θ.comp ϕ).sumElim (θ.comp ψ)
-- Mathlib.Algebra.Category.ModuleCat.Basic
linearEquivIsoModuleIso_hom : ∀ {R : Type u} [inst : Ring R] {X Y : Type u} [inst_1 : AddCommGroup X] [inst_2 : AddCommGroup Y] [inst_3 : Module R X]
  [inst_4 : Module R Y], linearEquivIsoModuleIso.hom = TypeCat.ofHom fun e => e.toModuleIso
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = true → t.minKey! = default
-- Mathlib.Topology.Maps.Strict.Basic
/-- A map is a strict map if and only if the canonical injection `Quotient (Setoid.ker f) → Y`
(`Setoid.kerLift f`) is an embedding.  -/
Topology.isStrictMap_iff_isEmbedding_kerLift : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsStrictMap f ↔ Topology.IsEmbedding (Setoid.kerLift f)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.decidableMemKer.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] [inst_2 : DecidableEq M] (f : G →+ M)
  (x : G), f.decidableMemKer x = decidable_of_iff (f x = 0) ⋯
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.sub` -/
CircleIntegrable.fun_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R → CircleIntegrable g c R → CircleIntegrable (fun i => f i - g i) c R
-- Mathlib.Analysis.ODE.PicardLindelof
IsPicardLindelof.continuousOn_uncurry : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K → ContinuousOn (Function.uncurry f) (Set.Icc tmin tmax ×ˢ Metric.closedBall x₀ ↑a)
-- Mathlib.Data.Finsupp.Basic
Finsupp.uncurry_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (a : α) (b : β) (m : M),
  (fun₀ | a => fun₀ | b => m).uncurry = fun₀ | (a, b) => m
-- Mathlib.Data.DFinsupp.WellFounded
Function.Lex.wellFoundedLT : ∀ {ι : Type u_1} {α : Type u_3} [inst : LinearOrder ι] [Finite ι] [inst_2 : LT α] [WellFoundedLT α],
  WellFoundedLT (Lex (ι → α))
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_le_iff : ∀ {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n), i.castPred hi ≤ j ↔ i ≤ j.castSucc
-- Init.Data.BitVec.Lemmas
BitVec.toInt_or : ∀ {w : ℕ} (x y : BitVec w), (x ||| y).toInt = (↑(x.toNat ||| y.toNat)).bmod (2 ^ w)
-- Std.Http.Data.Status
/-- 503 Service Unavailable
 -/
Std.Http.Status.serviceUnavailable : Std.Http.Status
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} [Std.TransCmp cmp] (t : RBTree.RBMap α β cmp) (k : α) (v : β)
  (k' : α), (t.insert k v).find? k' = if cmp k' k = Ordering.eq then some v else t.find? k'
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
algebra.  -/
CliffordAlgebra.toBaseChange : {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) →
                    CliffordAlgebra (QuadraticForm.baseChange A Q) →ₐ[A] TensorProduct R A (CliffordAlgebra Q)
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk' : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {n : ℕ} {R : L.Relations n} {i : ι}
  {x : Fin n → G i},
  (FirstOrder.Language.Structure.RelMap R fun a => ⟦FirstOrder.Language.Structure.Sigma.mk f i (x a)⟧) =
    FirstOrder.Language.Structure.RelMap R x
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom.sizeOf_spec : ∀ (α : Mathlib.Tactic.BicategoryLike.CoherenceHom),
  sizeOf (Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α) = 1 + sizeOf α
-- Lean.Util.InstantiateLevelParams
_private.Lean.Util.InstantiateLevelParams.0.Lean.Expr.getParamSubstArray : Array Lean.Name → Array Lean.Level → Lean.Name → ℕ → Option Lean.Level
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.desc.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)),
  CochainComplex.mappingCone.desc φ α β eq =
    (CochainComplex.mappingCone.descCocycle φ α (CochainComplex.HomComplex.Cocycle.ofHom β)
        CochainComplex.mappingCone.desc._proof_2 ⋯).homOf
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.liftGrindM : {α : Type} → Lean.Meta.Grind.GrindM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Dep.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.Dep D → D ⊆ M.E
-- Init.Prelude
instMonadExceptOfMonadExceptOf : (ε : Type u) → (m : Type v → Type w) → [MonadExceptOf ε m] → MonadExcept ε m
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.aemeasurable : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1},
  ProbabilityTheory.HasLaw X μ P → AEMeasurable X P
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation Q → P 2 ≠ 0 → Q 2 = 0 → W'.add P Q = -(Q 0 * P 2) • P
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_div : Primrec₂ fun x1 x2 => x1 / x2
-- Lean.Language.Basic
/-- Runs a tree of snapshots to conclusion,
folding the function `f` over each snapshot in tree preorder.  -/
Lean.Language.SnapshotTree.foldM : {m : Type u_1 → Type u_2} →
  {α : Type u_1} → [Monad m] → Lean.Language.SnapshotTree → (α → Lean.Language.Snapshot → m α) → α → m α
-- Lean.Parser.Tactic.Doc
/-- Validates that a tactic alternative is actually a tactic, that syntax tagged as tactics are
tactics, and that syntax with tactic names are tactics.
 -/
_private.Lean.Parser.Tactic.Doc.0.Lean.Parser.Tactic.Doc.tacticDocsOnTactics : Lean.Parser.ParserAttributeHook
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F) (x : TensorProduct 𝕜 E G),
  (ContinuousLinearMap.rTensor G f) x = (LinearMap.rTensor G ↑f) x
-- Init.Data.Option.Function
Option.map_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (Option.map f)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An abbreviation for `Π J, HasLimitsOfShape (Discrete J) C`  -/
CategoryTheory.Limits.HasProducts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Data.FinEnum
FinEnum.Finset.enum.eq_2 : ∀ {α : Type u} [inst : DecidableEq α] (x_1 : α) (xs : List α),
  FinEnum.Finset.enum (x_1 :: xs) = do
    let r ← FinEnum.Finset.enum xs
    [r, insert x_1 r]
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.eq = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.eq = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.eq = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.eq with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_2 ⋯
-- Mathlib.Topology.Clopen
IsClopen.isClosed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → IsClosed s
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.toOpenPartialHomeomorph_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [inst_5 : CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c)
  (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s),
  (ApproximatesLinearOn.toOpenPartialHomeomorph f s hf hc hs).target = f '' s
-- Std.Data.DTreeMap.Internal.Model
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minEntry?ₘ : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.forall_generateFrom_mem_iff_mem_iff : ∀ {α : Type u_1} {S : Set (Set α)} {x y : α},
  (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s
-- Std.Http.Data.URI.Encoding
Std.Http.Internal.Char.isHexDigitByte.eq_1 : ∀ (c : UInt8),
  Std.Http.Internal.Char.isHexDigitByte c =
    (decide (c ≥ '0'.toUInt8) && decide (c ≤ '9'.toUInt8) || decide (c ≥ 'a'.toUInt8) && decide (c ≤ 'f'.toUInt8) ||
      decide (c ≥ 'A'.toUInt8) && decide (c ≤ 'F'.toUInt8))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toList_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β},
  it.toList = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toList
        pure (out :: __do_lift)
      | Std.IterStep.skip it' => it'.toList
      | Std.IterStep.done => pure []
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
the obvious equivalence of categories
`w.StructuredArrowRightwards g ≌ w.CostructuredArrowDownwards g`.  -/
CategoryTheory.TwoSquare.equivalenceJ : {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₃) → w.StructuredArrowRightwards g ≌ w.CostructuredArrowDownwards g
-- Mathlib.LinearAlgebra.Prod
LinearMap.range_coprod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃), (f.coprod g).range = f.range ⊔ g.range
-- Init.Data.Int.Gcd
Int.lcm_eq_mul_div : ∀ (m n : ℤ), m.lcm n = m.natAbs * n.natAbs / m.gcd n