mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidMap_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f : M →+ N},
  Function.Injective ⇑f → ∀ (M' : AddSubmonoid M), Function.Injective ⇑(f.addSubmonoidMap M')
-- Mathlib.Data.Multiset.MapFold
Multiset.map_eq_cons : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β),
  (∃ a ∈ s, f a = b ∧ Multiset.map f (s.erase a) = t) ↔ Multiset.map f s = b ::ₘ t
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp : ∀ (R : Type u) [inst : CommSemiring R] (toFinsupp : AddMonoidAlgebra R ℕ),
  ((Polynomial.toFinsuppIsoAlg R).symm toFinsupp).toFinsupp = toFinsupp
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax left unity.  -/
CategoryTheory.LaxFunctor.map₂_leftUnitor_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X))
      ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X)
-- Mathlib.Topology.Order.MonotoneConvergence
InfConvergenceClass.mk : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  (∀ (a : α) (s : Set α), IsGLB s a → Filter.Tendsto Subtype.val Filter.atBot (nhds a)) → InfConvergenceClass α
-- Std.Time.Date.Unit.Weekday
/-- Sunday.  -/
Std.Time.Weekday.sunday : Std.Time.Weekday
-- Mathlib.Order.Defs.Unbundled
Maximal.eq_1 : ∀ {α : Type u_1} [inst : LE α] (P : α → Prop) (x : α), Maximal P x = (P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → y ≤ x)
-- Mathlib.RingTheory.Jacobson.Radical
Module.jacobson_le_of_eq_bot : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  Module.jacobson R (M ⧸ N) = ⊥ → Module.jacobson R M ≤ N
-- Init.Data.UInt.Bitwise
UInt32.zero_shiftLeft : ∀ {a : UInt32}, 0 <<< a = 0
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- When `ιObj I κ f` is considered as a relative `I`-cell complex,
the object at the `j`th step is obtained by applying the construction
`SmallObject.functorObj`.  -/
CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              {X Y : C} →
                (f : X ⟶ Y) →
                  (j : κ.ord.ToType) →
                    (CategoryTheory.SmallObject.relativeCellComplexιObj I κ f).F.obj (Order.succ j) ≅
                      CategoryTheory.SmallObject.functorObj I.homFamily
                        (((CategoryTheory.SmallObject.iterationFunctor I κ).obj j).obj (CategoryTheory.Arrow.mk f)).hom
-- Mathlib.Algebra.Module.TransferInstance
AddEquiv.linearEquiv_symm_apply : ∀ {α : Type u_2} {β : Type u_3} (A : Type u_4) [inst : Semiring A] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β]
  [inst_3 : Module A β] (e : α ≃+ β) (a : β), (AddEquiv.linearEquiv A e).symm a = e.invFun a
-- Mathlib.Geometry.Manifold.PoincareConjecture
_private.Mathlib.Geometry.Manifold.PoincareConjecture.0.term𝕊__ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.pi_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {ι : Type u_4} {φ : ι → Type u_5} [inst_4 : (i : ι) → TopologicalSpace (φ i)]
  [inst_5 : (i : ι) → AddCommMonoid (φ i)] [inst_6 : (i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) (c : M)
  (i : ι), (ContinuousLinearMap.pi f) c i = (f i) c
-- Init.Data.SInt.Bitwise
Int8.xor_comm : ∀ (a b : Int8), a ^^^ b = b ^^^ a
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_lt_d20 : Real.pi < 3.14159265358979323847
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_b₈_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).b₈ = W.b₈
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.mem_stabilizer_submodule_iff_map_eq : ∀ {R : Type u_4} {G : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Group G] [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] {S : Submodule R M} {e : G},
  e ∈ MulAction.stabilizer G S ↔ Submodule.map (DistribSMul.toLinearMap R M e) S = S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} {fallback : β} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filter! f t) k fallback =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_comp_map' : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : α → C} {h : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g]
  [inst_3 : CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (a : α) → f a ⟶ g a) (q' : (b : β) → g (p b) ⟶ h b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map' p q') =
    CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q (p b)) (q' b)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) (X : C), F.leftOpRightOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_of_set' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set Y} (hs : IsOpen s),
  e.trans (OpenPartialHomeomorph.ofSet s hs) = e.restr (e.source ∩ ↑e ⁻¹' s)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {J : Type u} [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j)
  (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k),
  (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse, version subtracting vectors.  -/
InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y = 0 → ‖x‖ / Real.cos (InnerProductGeometry.angle x (x - y)) = ‖x - y‖
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.monoidWithZero : {α : Type u_1} →
  [inst : Semiring α] →
    [inst_1 : PartialOrder α] → [ZeroLEOneClass α] → [AddLeftMono α] → [PosMulMono α] → MonoidWithZero { x // 0 ≤ x }
-- Mathlib.Data.Set.Function
Set.BijOn.bijective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.BijOn f s t),
  Function.Bijective (Set.MapsTo.restrict f s t ⋯)
-- Mathlib.Algebra.Group.Action.TypeTags
Additive.vadd : {α : Type u_2} → {β : Type u_3} → [SMul α β] → VAdd (Additive α) β
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_symm_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₁).symm (CategoryTheory.CategoryStruct.id r₁) =
    CategoryTheory.CategoryStruct.id l₁
-- Std.Data.Internal.List.Associative
Std.Internal.List.size_add_size_eq_size_insertList_add_size_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ →
      l₁.length + l₂.length =
        (Std.Internal.List.insertList l₁ l₂).length +
          (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).length
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_cons : ∀ {α : Type u} {L : List (α × Bool)} {a : α × Bool},
  FreeAddGroup.negRev (a :: L) = FreeAddGroup.negRev L ++ FreeAddGroup.negRev [a]
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.All_def : ∀ {α : Type u_1} {p : α → Prop} {t : RBTree.RBNode α}, RBTree.RBNode.All p t ↔ ∀ x ∈ t, p x
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
_private.Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing.0.ModularForm.E₄CubeSubE₆SqForm_isCuspForm : ModularForm.E₄CubeSubE₆SqForm✝.IsCuspForm
-- Mathlib.MeasureTheory.Integral.CircleIntegral
differentiable_circleMap : ∀ (c : ℂ) (R : ℝ), Differentiable ℝ (circleMap c R)
-- Init.Data.BitVec.Lemmas
BitVec.zero_sub : ∀ {n : ℕ} (x : BitVec n), 0#n - x = -x
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.eventuallyConst_smul_set_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α},
  Filter.EventuallyConst (c • s) (MeasureTheory.ae μ) ↔ Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Init.Prelude
/-- Evaluates a value from monad `m` into monad `n`.  -/
MonadEvalT.monadEval : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadEvalT m n] → {α : Type u} → m α → n α
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  P.universally = P ↔ P.IsStableUnderBaseChange
-- Mathlib.Algebra.FreeAlgebra
/-- The canonical function `X → FreeAlgebra R X`.
 -/
FreeAlgebra.ι : (R : Type u_3) → {X : Type u_4} → [inst : CommSemiring R] → X → FreeAlgebra R X
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (m : ℕ),
  Int.fract (a + ↑m) = Int.fract a
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.instNonemptyNOfNonempty : ∀ (X : SSet) [X.Nonempty], Nonempty X.N
-- Mathlib.Order.Filter.Partial
Filter.tendsto_iff_rtendsto' : ∀ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α → β),
  Filter.Tendsto f l₁ l₂ ↔ Filter.RTendsto' (Function.graph f) l₁ l₂
-- Std.Data.HashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.HashMap.Raw.inner : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Std.DHashMap.Raw α fun x => β
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_smul : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {G : Type u_3} [inst_3 : Monoid G]
  [inst_4 : MulSemiringAction G 𝔸] [ContinuousConstSMul G 𝔸] (g : G) (x : 𝔸),
  NormedSpace.exp (g • x) = g • NormedSpace.exp x
-- Init.Data.UInt.Lemmas
USize.size_sub_one_mod_uint16Size : (USize.size - 1) % UInt16.size = UInt16.size - 1
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing.congr_simp : ∀ (R : Type u) (ι : Type v) {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M] (z z_1 : M),
  z = z_1 → ContinuousMultilinearMap.mkPiRing R ι z = ContinuousMultilinearMap.mkPiRing R ι z_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℤ}, 2 < n.natAbs → ↑n ≠ 0 → 0 < (W.preΨ n).natDegree
-- Mathlib.Data.ENNReal.Basic
ENNReal.iInter_Ioi_coe_nat : ⋂ n, Set.Ioi ↑n = {⊤}
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
/-- Predicate on the triangle indices for there to be no accidental triangle.

Note that we cheat a bit, since the exact translation of this informal description would have
`(a', b', c') ∈ t` as a conclusion rather than `a = a' ∨ b = b' ∨ c = c'`. Those conditions are
equivalent when the explicit triangles are edge-disjoint (which is the case we care about).  -/
SimpleGraph.TripartiteFromTriangles.NoAccidental : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → Finset (α × β × γ) → Prop
-- Mathlib.Data.Set.Piecewise
Set.piecewise_le : ∀ {α : Type u_1} {δ : α → Type u_8} [inst : (i : α) → Preorder (δ i)] {s : Set α} [inst_1 : (j : α) → Decidable (j ∈ s)]
  {f₁ f₂ g : (i : α) → δ i}, (∀ i ∈ s, f₁ i ≤ g i) → (∀ i ∉ s, f₂ i ≤ g i) → s.piecewise f₁ f₂ ≤ g
-- Init.Data.Vector.Lex
Vector.instDecidableLEOfDecidableEqOfDecidableLT : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → [inst : LT α] → [DecidableLT α] → DecidableLE (Vector α n)
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mkState : (self : ShareCommon.StateFactoryImpl) → Unit → self.Map × self.Set
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppMatch.usingNames : {α : Type} →
  Array Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α → optParam ℕ 0 → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix.congr_simp : ∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommRing R] [inst_4 : Invertible 2] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (b b_1 : Module.Basis n R N),
  b = b_1 →
    ∀ (Q Q_1 : QuadraticForm R N),
      Q = Q_1 →
        ∀ (a a_1 : n),
          a = a_1 →
            ∀ (a_2 a_3 : n), a_2 = a_3 → QuadraticForm.toMatrix b Q a a_2 = QuadraticForm.toMatrix b_1 Q_1 a_1 a_3
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.hasBasis : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → (nhds 0).HasBasis (fun s => s ∈ p.basisSets) id
-- Mathlib.Order.RelIso.Set
RelIso.subrelUnivIso_apply : ∀ {α : Type u_1} {r : α → α → Prop} {p : α → Prop} (h : ∀ (x : α), p x) (x : Subtype p), (RelIso.subrelUnivIso h) x = ↑x
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.Expanded.proof.inj : ∀ {pf pf_1 : Lean.Term},
  Mathlib.Tactic.LinearCombinationPrime.Expanded.proof pf = Mathlib.Tactic.LinearCombinationPrime.Expanded.proof pf_1 →
    pf = pf_1
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddCommMonoid α],
  Shrink.instAddCommMonoid = (equivShrink α).symm.addCommMonoid
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.leadingCoeff_le_mapMahlerMeasure : ∀ {A : Type u_2} [inst : NormedRing A] (p : Polynomial A) (v : A →+* ℂ),
  Isometry ⇑v → ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
/-- In a nontrivial ring, `Matrix.mvPolynomialX m m R` has non-zero determinant.  -/
Matrix.det_mvPolynomialX_ne_zero : ∀ (m : Type u_1) (R : Type u_3) [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : CommRing R] [Nontrivial R],
  (Matrix.mvPolynomialX m m R).det ≠ 0
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.adjunction_counit_app : ∀ {R : CommRingCatᵒᵖ},
  AlgebraicGeometry.ΓSpec.adjunction.counit.app R = (AlgebraicGeometry.Scheme.ΓSpecIso (Opposite.unop R)).inv.op
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A notation for the Day convolution of two functors.  -/
CategoryTheory.MonoidalCategory.DayConvolution.«term_⊛_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.measurableSet_lt : ∀ {α : Type u_1} {E : Type u_5} {m : MeasurableSpace α} {f g : α → E} [inst : TopologicalSpace E] [inst_1 : Preorder E]
  [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasurableSet {a | f a < g a}
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The isomorphism `(K.truncLE' e).X i ≅ K.cycles i'` when `e.f i = i'`
and `e.BoundaryLE i` holds.  -/
HomologicalComplex.truncLE'XIsoCycles : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncLE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      {i : ι} → {i' : ι'} → e.f i = i' → e.BoundaryLE i → ((K.truncLE' e).X i ≅ K.cycles i')
-- Mathlib.Data.Set.Insert
Set.insert_union : ∀ {α : Type u_1} {s t : Set α} {a : α}, insert a s ∪ t = insert a (s ∪ t)
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.fibrations_over_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C) [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : CategoryTheory.Over S} (f : X ⟶ Y),
  HomotopicalAlgebra.Fibration f ↔ HomotopicalAlgebra.Fibration (CategoryTheory.Over.Hom.left f)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_mul_self_apply_self : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (i : V), (SimpleGraph.adjMatrix α G * SimpleGraph.adjMatrix α G) i i = ↑(G.degree i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst : Int.Internal.Linear.Var →
  Lean.Meta.Grind.Arith.Cutsat.EqCnstr →
    Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.Data.Stream.Init
Stream'.get_nats : ∀ (n : ℕ), Stream'.nats.get n = n
-- Mathlib.MeasureTheory.Group.Measure
/-- A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`.  -/
AddEquiv.isAddHaarMeasure_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [ContinuousAdd G] {H : Type u_3}
  [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H]
  [IsTopologicalAddGroup H] (e : G ≃+ H),
  Continuous ⇑e → Continuous ⇑e.symm → (MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.lift_quot_mk : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ M} (HN : N ≤ φ.ker) (g : G),
  (QuotientAddGroup.lift N φ HN) (Quot.mk (⇑(QuotientAddGroup.leftRel N)) g) = φ g
-- Init.Data.UInt.Lemmas
USize.add_left_inj : ∀ {a b : USize} (c : USize), a + c = b + c ↔ a = b
-- Mathlib.Topology.Order.LeftRightLim
/-- A monotone function is continuous at a point if and only if its left and right limits
coincide.  -/
Monotone.continuousAt_iff_leftLim_eq_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α],
      ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableAt.comp_differentiableWithinAt : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G},
  DifferentiableAt 𝕜 g (f x) → DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (g ∘ f) s x
-- Mathlib.RepresentationTheory.Coinvariants
Representation.toCoinvariants.congr_simp : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal],
  ρ.toCoinvariants S = ρ.toCoinvariants S
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk''.congr_simp : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W}
  (toContinuousLinearEquiv toContinuousLinearEquiv_1 : V ≃L[R] W)
  (e_toContinuousLinearEquiv : toContinuousLinearEquiv = toContinuousLinearEquiv_1)
  (cont : Continuous (↑↑toContinuousLinearEquiv).toFun)
  (isIntertwining' :
    ∀ (g : G),
      { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont } ∘SL π₁ g =
        π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont }),
  { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv_1, cont := ⋯, isIntertwining' := ⋯ }
-- Mathlib.Data.Fin.Basic
Fin.sub_succ_le_sub_of_le : ∀ {n : ℕ} {u v : Fin (n + 2)}, u < v → v - (u + 1) < v - u
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremsArray.isErased : {α : Type} → Lean.Meta.Grind.TheoremsArray α → Lean.Meta.Grind.Origin → Bool
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_eq_right_of_subset_of_measure_add_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  (μ + ν) t ≠ ⊤ → s ⊆ t → (μ + ν) s = (μ + ν) t → ν s = ν t
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C} (h : Z₁₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp v₁₂ (CategoryTheory.CategoryStruct.comp self.m₁ h) =
    CategoryTheory.CategoryStruct.comp u₂₃ (CategoryTheory.CategoryStruct.comp v₁₃ h)