mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ioc_ae_eq_Icc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, Set.Ioc a b =ᵐ[μ] Set.Icc a b
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.one_ne_zero : 1 ≠ 0
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.dual_contract_dual : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), (M✶.contract X)✶ = M.delete X
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_φ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ),
  (W.baseChange B).φ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).φ n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.size = t.size ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true),
      (f (t.getKey a h) (Std.DTreeMap.Internal.Impl.Const.get t a h)).isSome = true
-- Mathlib.Logic.Unique
unique_iff_existsUnique : ∀ (α : Sort u), Nonempty (Unique α) ↔ ∃! x, True
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSeparatedFor_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSeparatedFor P ⊤
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.const_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_7} [inst : NormedRing 𝕜] {f : α → 𝕜},
  MeasureTheory.HasFiniteIntegral f μ → ∀ (c : 𝕜), MeasureTheory.HasFiniteIntegral (fun x => c * f x) μ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Given an equivalence `e : R ≃+* S` of non-unital semirings and a non-unital subsemiring
`s` of `R`, `nonUnitalSubsemiringMap e s` is the induced equivalence between `s` and
`s.map e`  -/
RingEquiv.nonUnitalSubsemiringMap : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        (e : R ≃+* S) → (s : NonUnitalSubsemiring R) → ↥s ≃+* ↥(NonUnitalSubsemiring.map e.toNonUnitalRingHom s)
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.swap_mem_mulAntidiagonal : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  x.swap ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.ofIsoI_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) {I' : C} (e : F.I ≅ I')
  (F' : CategoryTheory.Limits.MonoFactorisation f),
  (hF.ofIsoI e).lift F' = CategoryTheory.CategoryStruct.comp e.inv (hF.lift F')
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (a : δ),
  Std.DHashMap.Internal.AssocList.forInStep.go✝ f Std.DHashMap.Internal.AssocList.nil a = pure (ForInStep.yield a)
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_zero : ∀ {M N : AddCommGrpCat}, AddCommGrpCat.Hom.hom 0 = 0
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Formula.isAtomic_graph : ∀ {L : FirstOrder.Language} {n : ℕ} (f : L.Functions n),
  FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Formula.graph f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.brecOn.go : {motive : Lean.Grind.CommRing.Expr → Sort u} →
  (t : Lean.Grind.CommRing.Expr) →
    ((t : Lean.Grind.CommRing.Expr) → Lean.Grind.CommRing.Expr.below t → motive t) →
      motive t ×' Lean.Grind.CommRing.Expr.below t
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.ext_iff' : ∀ {X : SSet} (s t : X.S), s = t ↔ ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens), I.radical.ideal U = (I.ideal U).radical
-- Mathlib.Algebra.Group.Units.Equiv
Units.coe_mapEquiv : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (h : M ≃* N) (x : Mˣ),
  ↑((Units.mapEquiv h) x) = h ↑x
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_prime : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, Nat.Prime p → pNilradical R p = nilradical R
-- Std.Data.DTreeMap.Internal.Cell
/-- Create an empty cell. Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.empty : {α : Type u} → {β : α → Type v} → [inst : Ord α] → {k : α → Ordering} → Std.DTreeMap.Internal.Cell α β k
-- Mathlib.Data.Set.Order
Antitone.union : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α},
  Antitone f → Antitone g → Antitone fun x => f x ∪ g x
-- Init.Control.Lawful.Basic
Id.ext_iff : ∀ {α : Type u_1} {x y : Id α}, x = y ↔ x.run = y.run
-- Mathlib.Analysis.Matrix.Normed
/-- This applies to the Frobenius norm.  -/
Matrix.frobeniusIsBoundedSMul : ∀ {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedRing R] [inst_3 : SeminormedAddCommGroup α] [inst_4 : Module R α] [IsBoundedSMul R α],
  IsBoundedSMul R (Matrix m n α)
-- Lean.Elab.Tactic.Conv.Pattern
_private.Lean.Elab.Tactic.Conv.Pattern.0.Lean.Elab.Tactic.Conv.pre : Lean.Meta.AbstractMVarsResult →
  IO.Ref Lean.Elab.Tactic.Conv.PatternMatchState → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitzOn.mono : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s t : Set α} {f : α → β},
  LocallyLipschitzOn t f → s ⊆ t → LocallyLipschitzOn s f
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postEquiv_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D), (CategoryTheory.Over.postEquiv X F).functor = CategoryTheory.Over.post F.functor
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer' : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.instInv.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H],
  Monoid.Coprod.instInv =
    {
      inv :=
        Quotient.map' (fun w => FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse)
          ⋯ }
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.inseparable_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [R1Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α},
  ContinuousAt f a → Inseparable (di.extend f (i a)) (f a)
-- Mathlib.Algebra.Star.Subalgebra
/-- The minimal star subalgebra that contains `s`.  -/
StarAlgebra.adjoin : (R : Type u_2) →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] → [inst_4 : StarRing A] → [inst_5 : StarModule R A] → Set A → StarSubalgebra R A
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_adjoin_of_mem : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {s : Set A} {x : A}, x ∈ s → x ∈ NonUnitalStarAlgebra.adjoin R s
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toAddEquiv : α ≃+ β)
  (map_le_map_iff' : ∀ {a b : α}, toAddEquiv.toFun a ≤ toAddEquiv.toFun b ↔ a ≤ b),
  sizeOf { toAddEquiv := toAddEquiv, map_le_map_iff' := map_le_map_iff' } = 1 + sizeOf toAddEquiv
-- Mathlib.NumberTheory.SmoothNumbers
/-- Membership in `Nat.factoredNumbers n` is decidable.  -/
Nat.instDecidablePredMemSetFactoredNumbers : (s : Finset ℕ) → DecidablePred fun x => x ∈ Nat.factoredNumbers s
-- Aesop.Util.Basic
Aesop.withAllTransparencySeqSyntax : Lean.Meta.TransparencyMode → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.path_unique : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ {v w : V} (p q : G.Path v w), p = q
-- Mathlib.CategoryTheory.Abelian.Basic
/-- In an abelian category, the pullback of an epimorphism is an epimorphism.
Proof from [aluffi2016, IX.2.3], cf. [borceux-vol2, 1.7.6]  -/
CategoryTheory.Abelian.epi_pullback_of_epi_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Tactic.Zify
/-- Translate a proof and the proposition into a zified form.  -/
Mathlib.Tactic.Zify.zifyProof : Option (Lean.Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") →
  Lean.Expr → Lean.Expr → Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_pow : ∀ (a : BitVec 64) (n : ℕ), { toBitVec := a ^ n } = { toBitVec := a } ^ n
-- Mathlib.Data.DFinsupp.BigOperators
/-- When summing over an `ZeroHom`, the decidability assumption is not needed, and the result is
also an `ZeroHom`.
 -/
DFinsupp.sumZeroHom : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → Zero (β i)] →
          [inst_1 : AddCommMonoid γ] → ((i : ι) → ZeroHom (β i) γ) → ZeroHom (Π₀ (i : ι), β i) γ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₃ = f.f₃.τ₂
-- Mathlib.Analysis.Normed.Operator.Banach
/-- If a bounded linear map is a bijection, then its inverse is also a bounded linear map.  -/
LinearEquiv.continuous_symm : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E] [inst_11 : RingHomInvPair σ' σ]
  (e : E ≃ₛₗ[σ] F), Continuous ⇑e → Continuous ⇑e.symm
-- Mathlib.Combinatorics.Digraph.Basic
/-- For digraphs `G`, `H`, `G ≤ H` iff `∀ a b, G.Adj a b → H.Adj a b`.  -/
Digraph.instLE : {V : Type u_2} → LE (Digraph V)
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.of_fact_finrank_eq_two : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Fact (Module.finrank K V = 2)], FiniteDimensional K V
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.isIndObject_of_isFiltered_of_finallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)]
  [CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)],
  CategoryTheory.Limits.IsIndObject A
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- Given a homological complex `K`, this is the property that the morphism
`K ⟶ K ⊞ K` induced by `𝟙 K` and `-𝟙 K` has a cofiber, which allows
to define `K.cylinder` as this cofiber.  -/
HomologicalComplex.HasCylinder : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] → Prop
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_eq_zero_iff_neg_eq : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit a → (a + b = 0 ↔ -a = b)
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.opEquivalence_counitIso : CategoryTheory.RelCat.opEquivalence.counitIso =
  CategoryTheory.Iso.refl (CategoryTheory.RelCat.unopFunctor.comp CategoryTheory.RelCat.opFunctor)
-- Mathlib.Algebra.Field.Defs
DivisionRing.toDivInvMonoid : {K : Type u_2} → [self : DivisionRing K] → DivInvMonoid K
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.condExp_le_nonneg_const : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : PartialOrder E] [ClosedIciTopology E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] {f : α → E} {c : E}, 0 ≤ c → (∀ᵐ (x : α) ∂μ, f x ≤ c) → ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c
-- Mathlib.Geometry.Euclidean.MongePoint
/-- This is an auxiliary lemma giving information about the relation
of two triangles in an orthocentric system; it abstracts some
reasoning, with no geometric content, that is common to some other
lemmas.  Suppose the orthocentric system is generated by triangle `t`,
and we are given three points `p` in the orthocentric system.  Then
either we can find indices `i₁`, `i₂` and `i₃` for `p` such that `p
i₁` is the orthocenter of `t` and `p i₂` and `p i₃` are points `j₂`
and `j₃` of `t`, or `p` has the same points as `t`.  -/
EuclideanGeometry.exists_of_range_subset_orthocentricSystem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P},
  t.orthocenter ∉ Set.range t.points →
    ∀ {p : Fin 3 → P},
      Set.range p ⊆ insert t.orthocenter (Set.range t.points) →
        Function.Injective p →
          (∃ i₁ i₂ i₃ j₂ j₃,
              i₁ ≠ i₂ ∧
                i₁ ≠ i₃ ∧
                  i₂ ≠ i₃ ∧
                    (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
                      p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
            Set.range p = Set.range t.points
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableWithinAt.mul` -/
DifferentiableWithinAt.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸},
  DifferentiableWithinAt 𝕜 a s x → DifferentiableWithinAt 𝕜 b s x → DifferentiableWithinAt 𝕜 (fun i => a i * b i) s x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limMap.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G),
  CategoryTheory.Limits.limMap α =
    CategoryTheory.Limits.IsLimit.map (CategoryTheory.Limits.limit.cone F) (CategoryTheory.Limits.limit.isLimit G) α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsAddMonHom.add_hom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M' N' : C}
  {inst_2 : CategoryTheory.AddMonObj M'} {inst_3 : CategoryTheory.AddMonObj N'} (f : M' ⟶ N')
  [self : CategoryTheory.IsAddMonHom f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
      CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_unzeroD : ∀ {α : Type u_1} [inst : PartialOrder α] {y : WithZero α} {a b : α}, ↑b ≤ y → b ≤ WithZero.unzeroD a y
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The morphism `S₁.cycles ⟶ S₂.cycles` induced by a morphism `S₁ ⟶ S₂` of short complexes.  -/
CategoryTheory.ShortComplex.cyclesMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        [inst_2 : S₁.HasLeftHomology] → [inst_3 : S₂.HasLeftHomology] → (S₁ ⟶ S₂) → (S₁.cycles ⟶ S₂.cycles)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_zero_iff_subsingleton : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam = 0 ↔ Subsingleton α
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_g : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (φ : R →+* S)
  (C : PrimeSpectrum.BasicConstructibleSetData R) (a : Fin C.n),
  (PrimeSpectrum.BasicConstructibleSetData.map φ C).g a = (⇑φ ∘ C.g) a
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ},
      0 ≤ f → ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in 0..A, y ∂MeasureTheory.Measure.map f μ
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Negating a matrix partitioned by columns is equivalent to negating each of the columns.  -/
Matrix.fromCols_neg : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Neg R] (A₁ : Matrix n m₁ R)
  (A₂ : Matrix n m₂ R), -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_repr_split : ∀ {o o' : ONote} {m : ℕ} [o.NF], o.split = (o', m) → o'.NF ∧ o.repr = o'.repr + ↑m
-- Init.Data.Vector.Count
Vector.countP_replace : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n} {p : α → Bool},
  Vector.countP p (xs.replace a b) =
    if xs.contains a = true then (Vector.countP p xs + if p b = true then 1 else 0) - if p a = true then 1 else 0
    else Vector.countP p xs
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
/-- If `Γ` acts properly discontinuously, so does every subgroup of `Γ`.  -/
instProperlyDiscontinuousSMulSubtypeMemSubgroup : ∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : SMul Γ α]
  [ProperlyDiscontinuousSMul Γ α] (G : Subgroup Γ), ProperlyDiscontinuousSMul (↥G) α
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.inf_dom_right : ∀ {α : Type ua} {β : Type ub} {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β},
  UniformContinuous f → UniformContinuous f
-- Mathlib.Order.Interval.Finset.Basic
/-- In a locally finite preorder, `≤` is the transitive closure of `⩿`.  -/
le_iff_transGen_wcovBy : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrder α] {x y : α},
  x ≤ y ↔ Relation.TransGen (fun x1 x2 => x1 ⩿ x2) x y
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.instInhabited : Inhabited MagmaCat
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ElimStatus.success.sizeOf_spec : sizeOf Mathlib.Tactic.Choose.ElimStatus.success = 1
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.State.mk.sizeOf_spec : ∀ (f fType : Lean.Expr) (fArgs : Array Lean.Expr) (args : List Lean.Elab.Term.Arg)
  (namedArgs : List Lean.Elab.Term.NamedArg) (expectedType? : Option Lean.Expr)
  (etaArgs : Array (Lean.Name × Lean.Expr)) (toSetErrorCtx instMVars : Array Lean.MVarId) (propagateExpected : Bool)
  (resultTypeOutParam? : Option Lean.MVarId) (foundNamedArgs : Array Lean.Name),
  sizeOf
      { f := f, fType := fType, fArgs := fArgs, args := args, namedArgs := namedArgs, expectedType? := expectedType?,
        etaArgs := etaArgs, toSetErrorCtx := toSetErrorCtx, instMVars := instMVars,
        propagateExpected := propagateExpected, resultTypeOutParam? := resultTypeOutParam?,
        foundNamedArgs := foundNamedArgs } =
    1 + sizeOf f + sizeOf fType + sizeOf fArgs + sizeOf args + sizeOf namedArgs + sizeOf expectedType? +
                sizeOf etaArgs +
              sizeOf toSetErrorCtx +
            sizeOf instMVars +
          sizeOf propagateExpected +
        sizeOf resultTypeOutParam? +
      sizeOf foundNamedArgs
-- Mathlib.Algebra.Exact.Basic
LinearEquiv.precomp_exact_iff_exact : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} {N : Type u_4} {P : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P]
  [inst_5 : Module R M] [inst_6 : Module R M'] [inst_7 : Module R N] [inst_8 : Module R P] {f : M →ₗ[R] N}
  {g : N →ₗ[R] P} {e : M' ≃ₗ[R] M}, Function.Exact ⇑(f ∘ₗ ↑e) ⇑g ↔ Function.Exact ⇑f ⇑g
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.uniqueAlgEquiv.congr_simp : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : Subsingleton M], MonoidAlgebra.uniqueAlgEquiv R M = MonoidAlgebra.uniqueAlgEquiv R M
-- Std.Data.Iterators.Combinators.DropWhile
/-- Constructs intermediate states of an iterator created with the combinator `Iter.dropWhile`.
When `it.dropWhile P` has stopped dropping elements, its new state cannot be created
directly with `Iter.dropWhile` but only with `Intermediate.dropWhile`.

`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.
 -/
Std.Iter.Intermediate.dropWhile : {β α : Type u_1} → (P : β → Bool) → Bool → Std.Iter β → Std.Iter β
-- Mathlib.Algebra.Group.Action.Defs
one_smul : ∀ (M : Type u_1) {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
-- Init.Data.BitVec.Lemmas
/-- `x.toInt` is greater than or equal to `-2^(w-1)`.
We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
 -/
BitVec.le_two_mul_toInt : ∀ {w : ℕ} {x : BitVec w}, -2 ^ w ≤ 2 * x.toInt
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.MorphismProperty.IsCompatibleWithShift.iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {A : Type w}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [W.IsCompatibleWithShift A] {X Y : C} (f : X ⟶ Y)
  (a : A), W ((CategoryTheory.shiftFunctor C a).map f) ↔ W f
-- Mathlib.Algebra.Group.Defs
AddGroup.mk : {A : Type u} → [toSubNegMonoid : SubNegMonoid A] → (∀ (a : A), -a + a = 0) → AddGroup A
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_symm_toRingHom : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p],
  (IsPerfectClosure.equiv i j p).symm.toRingHom = PerfectRing.lift j i p
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.smulLeft_apply_toLinearEquiv : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {G : Type u_9} [inst_4 : Group G] [inst_5 : DistribMulAction G M₁]
  [inst_6 : ContinuousConstSMul G M₁] [inst_7 : SMulCommClass G R₁ M₁] (g : G),
  ↑(ContinuousLinearEquiv.smulLeft g) = DistribMulAction.toLinearEquiv R₁ M₁ g