mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.discr'_comp`. -/
QuadraticForm.QuadraticMap.discr_comp : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  {Q : QuadraticForm R (n → R)} (f : (n → R) →ₗ[R] n → R),
  QuadraticForm.discr' (QuadraticMap.comp Q f) = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr'
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.length_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  (cs.leftInvSeq ω).length = ω.length
-- Mathlib.Data.Set.Finite.Lattice
/-- A finset is bounded below.  -/
Finset.bddBelow : ∀ {α : Type u} [inst : SemilatticeInf α] [Nonempty α] (s : Finset α), BddBelow ↑s
-- Mathlib.Order.SupIndep
Finset.supIndep_map : ∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : Lattice α] [inst_1 : OrderBot α] {f : ι → α} {s : Finset ι'}
  {g : ι' ↪ ι}, (Finset.map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)
-- Mathlib.ModelTheory.ElementaryMaps
/-- An elementary embedding is also a first-order embedding.  -/
FirstOrder.Language.ElementaryEmbedding.toEmbedding : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.ElementaryEmbedding M N → L.Embedding M N
-- Lean.Declaration
Lean.ConstantInfo.thmInfo.injEq : ∀ (val val_1 : Lean.TheoremVal), (Lean.ConstantInfo.thmInfo val = Lean.ConstantInfo.thmInfo val_1) = (val = val_1)
-- Mathlib.Data.Sum.Order
Sum.instReflLiftRel_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Refl r] [Std.Refl s],
  Std.Refl (Sum.LiftRel r s)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_iff_isChain_adj : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsClique s ↔ IsChain G.Adj s
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₀.X₃ = CategoryTheory.Limits.kernel g
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.β_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y : C),
  (β_ ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map (β_ X Y).hom)
        (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y X))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) [t.IsGE X a], t.IsGE ((t.truncGE b).obj X) a
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_union_sdiff_cancel'`.

---

A version of `sdiff_union_sdiff_cancel` with more general hypotheses.  -/
Set.diff_union_diff_cancel' : ∀ {α : Type u_1} {s t u : Set α}, s ∩ u ⊆ t → t ⊆ s ∪ u → s \ t ∪ t \ u = s \ u
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalClosure.congr_simp : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s s_1 : Submodule R M),
  s = s_1 → s.topologicalClosure = s_1.topologicalClosure
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- **Alias** of `SSet.quasicategory_of_innerFibration`.

---

[Kerodon Tag 01BJ](https://kerodon.net/tag/01BJ) -/
SSet.quasicategory_of_innerFibration_quasicategory : ∀ {X Y : SSet} (p : X ⟶ Y) [SSet.InnerFibration p] [hY : Y.Quasicategory], X.Quasicategory
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.nonMemberSubfamily_nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  Finset.nonMemberSubfamily a (Finset.nonMemberSubfamily a 𝒜) = Finset.nonMemberSubfamily a 𝒜
-- Mathlib.Data.Nat.Factorization.Basic
Nat.prod_primeFactors_pow_factorization : ∀ {n : ℕ}, n ≠ 0 → n = ∏ p ∈ n.primeFactors, p ^ n.factorization p
-- Mathlib.RingTheory.Derivation.MapCoeffs
/-- The unique derivation which can be made to a `DifferentialAlgebra` on `A[X]` with
`X′ = v`.
 -/
Differential.implicitDeriv : {A : Type u_1} → [inst : CommRing A] → [Differential A] → Polynomial A → Derivation ℤ (Polynomial A) (Polynomial A)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_addMonoidHom_id : ∀ {α : Type u_2} {x : NonAssocSemiring α}, ↑(RingHom.id α) = AddMonoidHom.id α
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.coe_toTwoSided : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], ↑I.toTwoSided = ↑I
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongrAut_apply : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (f : AddAut M),
  (AddMonoidAlgebra.domCongrAut R A) f = Additive.ofMul (AddMonoidAlgebra.domCongr R A f)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.alter.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f : Option (β a) → Option (β a))
  (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.alter a f x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil =>
      match f none with
      | none => Std.DHashMap.Internal.AssocList.nil
      | some b => Std.DHashMap.Internal.AssocList.cons a b Std.DHashMap.Internal.AssocList.nil
    | Std.DHashMap.Internal.AssocList.cons k v l =>
      if h : (k == a) = true then
        have h' := ⋯;
        match f (some (cast ⋯ v)) with
        | none => l
        | some b => Std.DHashMap.Internal.AssocList.cons a b l
      else
        have tail := Std.DHashMap.Internal.AssocList.alter a f l;
        Std.DHashMap.Internal.AssocList.cons k v tail
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_baseSet : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)], (e₁.prod e₂).baseSet = e₁.baseSet ∩ e₂.baseSet
-- Lean.Data.PPContext
Lean.PPContext.mk.sizeOf_spec : ∀ (env : Lean.Environment) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (opts : Lean.Options)
  (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl),
  sizeOf
      { env := env, mctx := mctx, lctx := lctx, opts := opts, currNamespace := currNamespace, openDecls := openDecls } =
    1 + sizeOf env + sizeOf mctx + sizeOf lctx + sizeOf opts + sizeOf currNamespace + sizeOf openDecls
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.head?.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (rank : ℕ) (val : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.head? le (Batteries.BinomialHeap.Imp.Heap.cons rank val c s) =
    some (Batteries.BinomialHeap.Imp.Heap.headD le val s)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instCommSemiring : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : CommMonoid G] →
        [inst_2 : MulSemiringAction G k] → [SMulCommClass G k k] → CommSemiring (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq J] (i : I) (j : J),
  p i ≠ j → X.ιMapObjOrZero p i j = 0
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- A bounded bilinear form `B` in a real normed space is *coercive*
if there is some positive constant C such that `C * ‖u‖ * ‖u‖ ≤ B u u`.
 -/
IsCoercive : {E : Type u_5} → [inst : SeminormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → (E →L[ℝ] E →L[ℝ] ℝ) → Prop
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_add_mul_right_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y + z * x) → IsCoprime x y
-- Mathlib.Algebra.Group.Action.Sum
Sum.instSMul.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β],
  Sum.instSMul = { smul := fun a => Sum.map (fun x => a • x) fun x => a • x }
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.eq_bot_or_vertexSet_nonempty : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), G = ⊥ ∨ G.vertexSet.Nonempty
-- Mathlib.Analysis.Normed.Group.Basic
/-- An analogue of `nnnorm_le_add_nnnorm_add` for the addition from the left.  -/
nnnorm_le_add_nnnorm_add' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖b‖₊ ≤ ‖a + b‖₊ + ‖a‖₊
-- Mathlib.Order.Filter.AtTopBot.Ring
exists_lt_mul_self : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] (a : R), ∃ x ≥ 0, a < x * x
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instQuiver : Quiver AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.finiteType : ∀ {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] (f : A) (d : ℕ),
  f ∈ 𝒜 d → Algebra.FiniteType (↥(𝒜 0)) (HomogeneousLocalization.Away 𝒜 f)
-- Init.Data.Vector.Zip
Vector.zipWith_self : ∀ {α : Type u_1} {δ : Type u_2} {n : ℕ} {f : α → α → δ} {xs : Vector α n},
  Vector.zipWith f xs xs = Vector.map (fun a => f a a) xs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} {k k' : α} {fallback : γ} (h : t.WF),
  t.getKey? k = some k' →
    Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k fallback =
      ((Std.DTreeMap.Internal.Impl.Const.get? t k).bind fun x => f k' x).getD fallback
-- Mathlib.Algebra.Order.Monovary
antivaryOn_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {v : α →₀ M} {f : α → β}
  {g : β → γ}, Finsupp.mapDomain (g ∘ f) v = Finsupp.mapDomain g (Finsupp.mapDomain f v)
-- Mathlib.Algebra.Star.Unitary
Unitary.val_toUnits_apply : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (x : ↥(unitary R)), ↑(Unitary.toUnits x) = ↑x
-- Mathlib.Data.Set.MulAntidiagonal
Set.swap_mem_antidiagonal_aux : ∀ {α : Type u_1} [inst : AddCommMagma α] {s t : Set α} {a : α} {x : α × α},
  x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 + x.1 = a ↔ x ∈ t.antidiagonal s a
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.triangle_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (CochainComplex.mappingCocone.triangle φ).obj₁ = CochainComplex.mappingCocone φ
-- Mathlib.Order.InitialSeg
/-- A principal segment is the same as a non-surjective initial segment.  -/
InitialSeg.toPrincipalSeg : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → [IsWellOrder β s] → (f : InitialSeg r s) → ¬Function.Surjective ⇑f → PrincipalSeg r s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k =
          Std.DHashMap.Internal.Raw₀.Const.get! m k
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bornology α] [inst_1 : Bornology β] [inst_2 : Bornology γ]
  {g : LocallyBoundedMap β γ} {f₁ f₂ : LocallyBoundedMap α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instCompleteLattice : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → CompleteLattice hI.SubDPIdeal
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_toSubsemigroup : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), H.op.toSubsemigroup = H.op
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' fallback : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else fallback else t.getKeyD k' fallback
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.MapSubtype.orderIso_apply_coe : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (H' : Subgroup ↥H),
  ↑((Subgroup.MapSubtype.orderIso H) H') = Subgroup.map H.subtype H'
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.isLocalHom_singleOneRingHom : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M], IsLocalHom MonoidAlgebra.singleOneRingHom
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side.  -/
Orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_iInf : ∀ {ι : Sort u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] (f : ι → ClosedSubmodule R M), ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
AEMeasurable.eval : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {δ : Type u_6} {X : δ → Type u_7}
  {mX : (a : δ) → MeasurableSpace (X a)} {g : α → (a : δ) → X a},
  AEMeasurable g μ → ∀ (a : δ), AEMeasurable (fun x => g x a) μ
-- Mathlib.Logic.Function.Basic
Pi.map_injective : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} [∀ (i : ι), Nonempty (α i)] {f : (i : ι) → α i → β i},
  Function.Injective (Pi.map f) ↔ ∀ (i : ι), Function.Injective (f i)
-- Init.PropLemmas
exists_eq_right' : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, p a ∧ a' = a) ↔ p a'
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.LeftHomotopyRel f g → ∃ P, P.IsVeryGood ∧ Nonempty (P.LeftHomotopy f g)
-- Lean.Meta.Transform
/-- Like `Meta.transform`, but accepts and returns a cache for reuse across multiple calls.

Parameters:
- `usedLetOnly`: when true, `mkLambdaFVars`/`mkForallFVars`/`mkLetFVars` only abstract
  over variables that are actually used in the body.
- `skipConstInApp`: when true, constant heads in applications are not visited separately.
- `skipInstances`: when true, instance arguments (determined via `getFunInfo`) are not visited.

The `skipInstances` flag is used by `dsimp` to avoid rewriting instances.

**Warnings:**
- The cache is only valid when using the same `pre` and `post` functions.
- Ensure there are no other references to `cache` to avoid unnecessary hash map copying.
 -/
Lean.Meta.transformWithCache : {m : Type → Type} →
  [inst : Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        Lean.Expr →
          Std.HashMap Lean.ExprStructEq Lean.Expr →
            (optParam (Lean.Expr → m Lean.TransformStep) fun x => pure Lean.TransformStep.continue) →
              (optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) →
                optParam Bool false →
                  optParam Bool false → optParam Bool false → m (Lean.Expr × Std.HashMap Lean.ExprStructEq Lean.Expr)
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta.eq_1 : ArithmeticFunction.zeta = { toFun := fun x => if x = 0 then 0 else 1, map_zero' := ArithmeticFunction.zeta._proof_1 }
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.UniversallyOpen
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Natural transformations from a constant presheaf into a sheaf correspond to morphisms to its
global sections.  -/
CategoryTheory.Sheaf.ΓHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] →
              {X : A} →
                {F : CategoryTheory.Sheaf J A} →
                  ((CategoryTheory.Functor.const Cᵒᵖ).obj X ⟶ F.obj) ≃ (X ⟶ (CategoryTheory.Sheaf.Γ J A).obj F)
-- Mathlib.Tactic.FunProp.Types
/-- Default names to be considered reducible by `fun_prop`  -/
Mathlib.Meta.FunProp.defaultNamesToUnfold : Array Lean.Name
-- Mathlib.NumberTheory.Harmonic.Bounds
harmonic_le_one_add_log : ∀ (n : ℕ), ↑(harmonic n) ≤ 1 + Real.log ↑n
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.exists_mem_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Finset α)},
  𝒜.Intersecting → ∀ {s t : Finset α}, s ∈ 𝒜 → t ∈ 𝒜 → ∃ a ∈ s, a ∈ t
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivOfCompEqX_eq_iff : ∀ {R : Type u} [inst : CommSemiring R] (p q p' q' : Polynomial R) (hpq : p.comp q = Polynomial.X)
  (hqp : q.comp p = Polynomial.X) (hpq' : p'.comp q' = Polynomial.X) (hqp' : q'.comp p' = Polynomial.X),
  p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp' ↔ p = p'
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
  [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize) →
    Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass) →
      ∀ (f : BoundedContinuousFunction Ω NNReal),
        Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₁ : Lean.Expr → Lean.Expr → ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM Bool
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.coe_m_add_one_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ},
  0 < ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- Expansion of `log (1 + a)` as a series in powers of `a / (a + 2)`.  -/
Real.hasSum_log_one_add : ∀ {a : ℝ}, 0 ≤ a → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (Real.log (1 + a))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_isoColimit_inv : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasColimit X]
  (j : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j })
      (CategoryTheory.Limits.Sigma.isoColimit X).inv =
    CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.congr_toLinearEquiv : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D),
  ↑(Algebra.TensorProduct.congr f g) = TensorProduct.AlgebraTensorModule.congr ↑f ↑g
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The cone of `F` corresponding to an element in `(F ⋙ yoneda.obj X).sections`.  -/
CategoryTheory.Limits.coneOfSectionCompYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          (X : C) → ↑(F.comp (CategoryTheory.yoneda.obj X)).sections → CategoryTheory.Limits.Cone F
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instNorm : {E : Type u_2} → [inst : SeminormedAddCommGroup E] → Norm (SeparationQuotient E)
-- Batteries.Data.List.Count
List.count_singleton' : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α), List.count a [b] = if b = a then 1 else 0
-- Init.Data.String.Lemmas.Basic
String.Slice.pos.congr_simp : ∀ (s : String.Slice) (off off_1 : String.Pos.Raw) (e_off : off = off_1) (h : String.Pos.Raw.IsValidForSlice s off),
  s.pos off h = s.pos off_1 ⋯
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.neg : ∀ {G : Type u_4} [inst : InvolutiveNeg G] [inst_1 : TopologicalSpace G] [ContinuousNeg G] {s : Set G} {a b : G},
  JoinedIn s a b → JoinedIn (-s) (-a) (-b)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.HomotopyCategory₂.mk.inj : ∀ {A : SSet.Truncated 2}
  {pt pt_1 : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })},
  { pt := pt } = { pt := pt_1 } → pt = pt_1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.indep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.Indep I