mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Topology.Bases
TopologicalSpace.secondCountableTopology_iInf : ∀ {α : Type u_1} {ι : Sort u_2} [Countable ι] {t : ι → TopologicalSpace α},
  (∀ (i : ι), SecondCountableTopology α) → SecondCountableTopology α
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_lt_toReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toReal < b.toReal ↔ a < b)
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.coe_opLinearEquiv_addEquiv : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.zero_vlt_coe_posSubmonoid : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : ↥(ValuativeRel.posSubmonoid R)), 0 <ᵥ ↑x
-- Mathlib.Topology.MetricSpace.Infsep
Set.nontrivial_of_einfsep_ne_top : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep ≠ ⊤ → s.Nontrivial
-- Init.Data.SInt.Lemmas
Int8.toInt_ofIntLE : ∀ {x : ℤ} {h₁ : Int8.minValue.toInt ≤ x} {h₂ : x ≤ Int8.maxValue.toInt}, (Int8.ofIntLE x h₁ h₂).toInt = x
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`
(and moreover the function is analytic when `n = ω`).  -/
contDiffWithinAt_succ_iff_hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  n ≠ ↑⊤ →
    (ContDiffWithinAt 𝕜 (n + 1) f s x ↔
      ∃ u ∈ nhdsWithin x (insert x s),
        (n = ⊤ → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x)
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_self : ∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [inst_1 : CommRing L] (i : K →+* L) (p : ℕ) [inst_2 : ExpChar K p]
  [inst_3 : IsPRadical i p] [inst_4 : ExpChar L p] [inst_5 : PerfectRing L p], PerfectRing.lift i i p = RingHom.id L
-- Mathlib.Topology.Order.DenselyOrdered
interior_Iic' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Ioi a).Nonempty → interior (Set.Iic a) = Set.Iio a
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State : Type
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- An auxiliary bilinear map that is later passed into `CliffordAlgebra.foldr`. Our desired result
is stored in the `A` part of the accumulator, while auxiliary recursion state is stored in the `S f`
part.  -/
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Even.0.CliffordAlgebra.even.lift.fFold : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} →
            {A : Type u_3} →
              [inst_3 : Ring A] →
                [inst_4 : Algebra R A] →
                  (f : CliffordAlgebra.EvenHom Q A) →
                    M →ₗ[R] A × ↥(CliffordAlgebra.even.lift.S✝ f) →ₗ[R] A × ↥(CliffordAlgebra.even.lift.S✝ f)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.instNonemptySphere : ∀ {P : Type u_2} [inst : MetricSpace P] [Nonempty P], Nonempty (EuclideanGeometry.Sphere P)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.prodMap : ∀ {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z'] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Z, Z')},
  f₀.Homotopic f₁ → g₀.Homotopic g₁ → (f₀.prodMap g₀).Homotopic (f₁.prodMap g₁)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        m.contains k = false →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey? k' = some k
-- Lean.Meta.Eqns
Lean.Meta.eqnThmSuffixBase : String
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_mul_eq_vecMul : ∀ {m : Type u_1} {n : Type u_2} {p : Type u_4} {R : Type u_3} [inst : Semiring R] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : DecidableEq m] (A : Matrix m n R) (B : Matrix n p R),
  (A * B).vec = Matrix.vecMul A.vec (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B 1)
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.toListRev_iter : ∀ {β : Type w} {array : Array β}, array.iter.toListRev = array.toListRev
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.ext : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] ⦃f g : LocallyConstant X Y⦄, (∀ (x : X), f x = g x) → f = g
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.finrank_dvd_of_le_left : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E : IntermediateField K L}, F ≤ E → Module.finrank (↥E) L ∣ Module.finrank (↥F) L
-- Mathlib.Order.LatticeIntervals
Set.Ici.boundedOrder : {α : Type u_1} → [inst : Preorder α] → [OrderTop α] → {a : α} → BoundedOrder ↑(Set.Ici a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_left_hom : ∀ {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₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  (iso : f₁ ≅ f₁'), (sq₁₃.π_iso_of_iso_left sq₁₃' iso).hom = sq₁₃.mapArrowLeft sq₁₃' iso.inv
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] [inst_5 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β k → β k},
      Std.Internal.List.minKey! (Std.Internal.List.modifyKey k f l) = Std.Internal.List.minKey! l
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instLTIProp : LT Mathlib.Tactic.ITauto.IProp
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashSet.ofList l).getD k' fallback = k
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimMap_eq : ∀ {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.HasColimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G), CategoryTheory.Limits.colimMap α = CategoryTheory.Limits.colim.map α
-- Std.Time.Format
/-- The leanDateTimeWithIdentifier format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss[z]`
for representing date, time, and time zone. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDateTimeWithIdentifier : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.coe_mul_self_eq : ∀ {M : Type u_3} [inst : Monoid M] (s : Submonoid M), ↑s * ↑s = ↑s
-- Mathlib.LinearAlgebra.Multilinear.Curry
LinearMap.curry_uncurryLeft : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  (f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂), f.uncurryLeft.curryLeft = f
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.num_zero_eq : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  Function.Injective ⇑(algebraMap R P) → FractionalIdeal.num 0 = 0
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff.inj : ∀ {R : Type u_1} {M : Type u_2} {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {coeff coeff_1 : ℕ →₀ M}, { coeff := coeff } = { coeff := coeff_1 } → coeff = coeff_1
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `ν` is an s-finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }`
is a measurable function.

Not true without the s-finite assumption: on `ℝ × ℝ` with the product sigma-algebra, let `s` be the
diagonal and let `ν` be an uncountable sum of Dirac measures (all Dirac measures for points in a
set `t`). Then `ν (Prod.mk x ⁻¹' s) = ν {x} = if x ∈ t then 1 else 0`. If `t` is chosen
non-measurable, this will not be measurable.  -/
measurable_measure_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {s : Set (α × β)}, MeasurableSet s → Measurable fun x => ν (Prod.mk x ⁻¹' s)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The algebra isomorphism `adjoin ℤ {ζ} ≃ₐ[ℤ] (𝓞 K)`, where `ζ` is a primitive `p ^ k`-th root of
unity and `K` is a `p ^ k`-th cyclotomic extension of `ℚ`.  -/
IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow : {p k : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [hp : Fact (Nat.Prime p)] →
          [inst_1 : CharZero K] →
            [IsCyclotomicExtension {p ^ k} ℚ K] → IsPrimitiveRoot ζ (p ^ k) → ↥ℤ[ζ] ≃ₐ[ℤ] NumberField.RingOfIntegers K
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1`, then `smoothingFun μ x` is nonnegative.  -/
smoothingFun_nonneg : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R), μ 1 ≤ 1 → ∀ (x : R), 0 ≤ smoothingFun μ x
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableNeg : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : (i : ι) → Neg (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableNeg (α i)], MeasurableNeg ((i : ι) → α i)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.sumArrowEquivProdArrow_apply : ∀ {α : Type u_2} {β : Type u_3} {R : Type u_4} [inst : NonAssocSemiring R] (x : α ⊕ β → R),
  (RingEquiv.sumArrowEquivProdArrow α β R) x = (Equiv.sumArrowEquivProdArrow α β R) x
-- Mathlib.Tactic.TautoSet
/-- `specialize_all x` runs `specialize h x` for all hypotheses `h` where this tactic succeeds.
 -/
Mathlib.Tactic.TautoSet.specialize_all : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- Preserving cofiltered limits at any universe implies preserving cofiltered limits at universe `0`.
 -/
CategoryTheory.Limits.preservesSmallestCofilteredLimits_of_preservesCofilteredLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Mathlib.Algebra.Group.Equiv.Defs
instCoeTCMulEquivOfMulEquivClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : MulEquivClass F α β], instCoeTCMulEquivOfMulEquivClass = { coe := MulEquivClass.toMulEquiv }
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.isoMk_inv : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G),
  (CategoryTheory.Cat.Hom.isoMk e).inv = CategoryTheory.NatTrans.toCatHom₂ e.inv
-- Mathlib.Topology.ContinuousOn
continuousAt_prod_of_discrete_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} {x : α × β},
  ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x_1, x.2)) x.1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instSemilatticeSup : {K : Type u} → [inst : Field K] → SemilatticeSup (ValuationSubring K)
-- Mathlib.Algebra.Category.Ring.Limits
CommRingCat.forget₂Ring_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommRingCat RingCat)
-- Init.Data.Ord.Basic
instReprOrdering : Repr Ordering
-- Mathlib.Algebra.Order.Group.Defs
eq_zero_of_neg_eq : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, -a = a → a = 0
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_zero_of_le_one : ∀ {x : ℝ}, x ≤ 1 → Chebyshev.theta x = 0
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- If `δ` is small enough, a `(1-δ)`-separated set in the ball of radius `2` also has cardinality
at most `multiplicity E`.  -/
Besicovitch.exists_goodδ : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  ∃ δ,
    0 < δ ∧
      δ < 1 ∧
        ∀ (s : Finset E),
          (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) → s.card ≤ Besicovitch.multiplicity E
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.del.match_1.eq_1 : ∀ (motive : RBTree.RBColor → Sort u_1) (h_1 : Unit → motive RBTree.RBColor.black)
  (h_2 : Unit → motive RBTree.RBColor.red),
  (match RBTree.RBColor.black with
    | RBTree.RBColor.black => h_1 ()
    | RBTree.RBColor.red => h_2 ()) =
    h_1 ()
-- Mathlib.RingTheory.Congruence.Basic
/-- The inductively defined smallest congruence relation containing a binary relation `r` equals
the infimum of the set of congruence relations containing `r`.  -/
RingCon.ringConGen_eq : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (r : R → R → Prop),
  ringConGen r = sInf {s | ∀ (x y : R), r x y → s x y}
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The image of zero is zero.  -/
AddGroupSeminorm.map_zero' : ∀ {G : Type u_6} [inst : AddGroup G] (self : AddGroupSeminorm G), self.toFun 0 = 0
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.isCoprime_of_dvd_isCoprime : ∀ {d : ℤ} {a b : ℤ√d}, IsCoprime a.re a.im → b ∣ a → IsCoprime b.re b.im
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_iff_le_not_ge` -/
ssubset_iff_subset_not_superset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a
-- Aesop.RuleSet
Aesop.mkLocalRuleSet : Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name) → Aesop.Options' → Lean.CoreM Aesop.LocalRuleSet
-- Mathlib.Data.Finmap
Finmap.union.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s₁ s₂ : Finmap β),
  s₁.union s₂ = s₁.liftOn₂ s₂ (fun s₁ s₂ => (s₁ ∪ s₂).toFinmap) ⋯
-- Mathlib.ModelTheory.Definability
Set.definable_finset_sup : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2}
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → ∀ (s : Finset ι), A.Definable L (s.sup f)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_eq_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a : G →₀ k}, { coeff := a } = 0 ↔ a = 0
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.op_epi_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi f.op ↔ CategoryTheory.Mono f
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q.ind : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {β : Lean.Grind.Ring.OfSemiring.Q α → Prop},
  (∀ (a : α × α), β (Lean.Grind.Ring.OfSemiring.Q.mk a)) → ∀ (q : Lean.Grind.Ring.OfSemiring.Q α), β q
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.IsKProjective.homotopyZero_def : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) (hL : HomologicalComplex.Acyclic L) [inst_2 : K.IsKProjective],
  CochainComplex.IsKProjective.homotopyZero f hL = ⋯.some
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notStrictValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.ext : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (W W' : CategoryTheory.MorphismProperty C),
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) → W = W'
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Icc_eq_Iic_self_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α} {a : α},
  ⋃ i, Set.Icc (f i) a = Set.Iic a ↔ ∀ (x : α), a ≥ x → ∃ i, f i ≤ x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- See `measurable_from_prod_countable_left` for a version where we assume that singletons are
measurable instead of reasoning about `measurableAtom`.  -/
measurable_from_prod_countable_left' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [Countable β] {f : α × β → γ},
  (∀ (y : β), Measurable fun x => f (x, y)) →
    (∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)) → Measurable f
-- Mathlib.Tactic.ITauto
/-- Once we have a proof object, we have to apply it to the goal.  -/
Mathlib.Tactic.ITauto.applyProof : Lean.MVarId → Lean.NameMap Lean.Expr → Mathlib.Tactic.ITauto.Proof → Lean.MetaM Unit
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.contains_bool_eq : ∀ {p : Char → Bool} {s : String}, s.contains p = s.toList.any p
-- Mathlib.Order.Circular
OrderDual.btw : (α : Type u_1) → [h : Btw α] → Btw αᵒᵈ
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.mk : Array Aesop.Subgoal →
  Lean.Meta.SavedState → Option (Array Aesop.Script.LazyStep) → Option Aesop.Percent → Aesop.RuleApplication
-- Lean.Parser.Basic
Lean.Parser.withoutInfo : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Topology.Irreducible
/-- [Stacks Tag 004W](https://stacks.math.columbia.edu/tag/004W) ((4)) -/
mem_irreducibleComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, x ∈ irreducibleComponent x
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.inter : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (self : Besicovitch.SatelliteConfig α N τ),
  ∀ i < Fin.last N, dist (self.c i) (self.c (Fin.last N)) ≤ self.r i + self.r (Fin.last N)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.π_f_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
  P.π.f (n + 1) = 0
-- Mathlib.Order.Interval.Finset.Basic
/-- This is a special case of `Ico_union_Ico`  -/
Finset.Ico_union_Ico' : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  c ≤ b → a ≤ d → Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeGroup : ∀ (α : Type u) [Countable α], Countable (FreeGroup α)
-- Mathlib.Algebra.Group.PUnit
PUnit.sub_eq : ∀ (x y : PUnit.{u_1 + 1}), x - y = PUnit.unit
-- Mathlib.GroupTheory.Index
/-- Typeclass for finite index subgroups.  -/
Subgroup.FiniteIndex : {G : Type u_1} → [inst : Group G] → Subgroup G → Prop
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.instHasPullbacksSingletonOfHasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [CategoryTheory.Limits.HasPullback g f], (CategoryTheory.Presieve.singleton g).HasPullbacks f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_singleton_iff : ∀ {k m n : ℕ}, (m...=n).toArray = #[k] ↔ n = m ∧ m = k
-- Init.Tactics
/-- Similar to `have`, but using `refine'`  -/
Lean.Parser.Tactic.tacticHave' : Lean.ParserDescr
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.age.fg_substructure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M},
  S.FG → { α := ↥S, str := inferInstance } ∈ L.age M
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.coe_toOpens : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U : OpenAddSubgroup G}, ↑↑U = ↑U
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {U V : Set X}, JoinedIn U x y → U ⊆ V → JoinedIn V x y
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressProcessingInfo.mk.inj : ∀ {range : Lean.Lsp.Range} {kind : Lean.Lsp.LeanFileProgressKind} {range_1 : Lean.Lsp.Range}
  {kind_1 : Lean.Lsp.LeanFileProgressKind},
  { range := range, kind := kind } = { range := range_1, kind := kind_1 } → range = range_1 ∧ kind = kind_1
-- Mathlib.Order.Filter.Pi
Filter.mem_pi_of_mem : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} (i : ι) {s : Set (α i)},
  s ∈ f i → Function.eval i ⁻¹' s ∈ Filter.pi f
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.cyclesFunctor C).obj S = S.cycles
-- Mathlib.Condensed.Discrete.Colimit
/-- `lanPresheafIso` is natural in `S`.  -/
Condensed.lanPresheafNatIso : {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} →
  ((S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) → (Condensed.lanPresheaf F ≅ F)
-- Init.Data.String.Lemmas.Basic
String.Slice.pos!_eq_pos : ∀ {s : String.Slice} {p : String.Pos.Raw} (h : String.Pos.Raw.IsValidForSlice s p), s.pos! p = s.pos p h
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- basic open sets in `Spec`  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.termSbo_ : Lean.ParserDescr
-- Mathlib.Data.EReal.Inv
EReal.div_zero : ∀ {a : EReal}, a / 0 = 0
-- Aesop.EMap
Aesop.EMap.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (rep : Lean.PArray (Option (Lean.Expr × α))) (idx : Lean.Meta.DiscrTree ℕ),
  sizeOf { rep := rep, idx := idx } = 1 + sizeOf rep + sizeOf idx
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpace_zero_normalizer_eq_self : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L], (LieModule.genWeightSpace M 0).normalizer = LieModule.genWeightSpace M 0
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSets_singleton_iff : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s t : Set Ω},
  ProbabilityTheory.IndepSets {s} {t} μ ↔ μ (s ∩ t) = μ s * μ t
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `Set.Pairwise.insert_of_symm`. -/
Set.Pairwise.insert_of_symmetric : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  s.Pairwise r → (∀ b ∈ s, a ≠ b → r a b) → (insert a s).Pairwise r
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_y : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution.y✝ S