mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.snd_sum : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (s : Multiset (M × N)),
  s.sum.2 = (Multiset.map Prod.snd s).sum
-- Init.Data.Rat.Lemmas
Rat.mul_pos_iff_of_pos_left : ∀ {a b : ℚ}, 0 < a → (0 < a * b ↔ 0 < b)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.LocallyLinear.card_edgeFinset : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : DecidableRel G.Adj],
  G.LocallyLinear → G.edgeFinset.card = 3 * (G.cliqueFinset 3).card
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a Galois group on `L/K` and `L/E/K` is a tower of field extensions,
then the fixing subgroup of the image of `E` in `L` is a Galois group on `L/E`.  -/
IsGaloisGroup.of_isScalarTower : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L] (E : Type u_5)
  [inst_7 : Field E] [inst_8 : Algebra K E] [inst_9 : Algebra E L] [IsScalarTower K E L],
  IsGaloisGroup (↥(fixingSubgroup G (Set.range ⇑(algebraMap E L)))) E L
-- Mathlib.Algebra.GroupWithZero.Defs
mul_eq_zero_of_right : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] (a : M₀) {b : M₀}, b = 0 → a * b = 0
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_compl_iff : ∀ {α : Type u_1} [inst : LE α] {s : UpperSet α} {a : α}, a ∈ s.compl ↔ a ∉ s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.exists_of_liftRel_right : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s t → ∀ {b : β}, b ∈ t → ∃ a ∈ s, R a b
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- A primitive additive character on `ZMod n` takes the value `1` only at `0`.  -/
AddChar.IsPrimitive.zmod_char_eq_one_iff : ∀ {C : Type v} [inst : CommMonoid C] (n : ℕ) [NeZero n] {ψ : AddChar (ZMod n) C},
  ψ.IsPrimitive → ∀ (a : ZMod n), ψ a = 1 ↔ a = 0
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r.injEq : ∀ {n : ℕ} (a a_1 : ZMod n), (DihedralGroup.r a = DihedralGroup.r a_1) = (a = a_1)
-- Lean.Data.Json.Printer
Lean.Json.pretty : Lean.Json → optParam ℕ 80 → String
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.left_of_add_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.MemLp f p (μ + ν) → MeasureTheory.MemLp f p μ
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Preconnected.ofBoxProdRight : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [Nonempty α],
  (G □ H).Preconnected → H.Preconnected
-- Mathlib.Algebra.Algebra.Hom
AlgHom.End : {R : Type u} →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Monoid (A →ₐ[R] A)
-- Init.Data.List.Sublist
List.sublist_append_left : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁.Sublist (l₁ ++ l₂)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.priority.quot : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
ContDiff.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞},
  ContDiff ℝ (↑n) f → ContDiff ℝ ↑n fun x => Real.arctan (f x)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instEssSurjCompPostOfFull : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) [F.Full], (CategoryTheory.Comma.post L R F).EssSurj
-- Lean.Parser.Term
/-- A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.

A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
 -/
Lean.Parser.Command.docComment : Lean.Parser.Parser
-- Mathlib.Probability.Independence.Basic
/-- Two sets of sets `s₁, s₂` are independent with respect to a measure `μ` if for any sets
`t₁ ∈ p₁, t₂ ∈ s₂`, then `μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)`  -/
ProbabilityTheory.IndepSets : {Ω : Type u_1} →
  {_mΩ : MeasurableSpace Ω} →
    Set (Set Ω) → Set (Set Ω) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepSets._auto_1 → Prop
-- Mathlib.RingTheory.TensorProduct.Free
/-- Given an `R`-algebra `A`, this is the `A`-basis of `A ⊗[R] M` induced by an `R`-basis of `M`.  -/
Algebra.TensorProduct.basis : {R : Type u_1} →
  (A : Type u_2) →
    {M : Type uM} →
      {ι : Type uι} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module R M] → Module.Basis ι R M → Module.Basis ι A (TensorProduct R A M)
-- Init.Data.Int.DivMod.Lemmas
Int.lt_ediv_mul : ∀ (a : ℤ) {b : ℤ}, 0 < b → a - b < a / b * b
-- Mathlib.RingTheory.Noetherian.Defs
/-- A module is Noetherian iff every increasing chain of submodules stabilizes.  -/
monotone_stabilizes_iff_noetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_mul_intCast : ∀ (x : NNReal) (y : ℝ) (n : ℤ), x ^ (y * ↑n) = (x ^ y) ^ n
-- Mathlib.Data.Fintype.Card
Prop.instWellFoundedGT : WellFoundedGT Prop
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.ipv4.injEq : ∀ (ipv4 ipv4_1 : Std.Net.IPv4Addr), (Std.Http.URI.Host.ipv4 ipv4 = Std.Http.URI.Host.ipv4 ipv4_1) = (ipv4 = ipv4_1)
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_lt_left : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M}, a < b → ∀ (c : M), a + c < b + c
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.Lex.isOrderedAddCancelMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β],
  IsOrderedCancelAddMonoid (Lex (α × β))
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_elim_cert : ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.div_spanSingleton : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] (J : FractionalIdeal (nonZeroDivisors R₁) K) (d : K),
  J / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) d = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) d⁻¹ * J
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpiCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f) → CategoryTheory.SplitEpiCategory C
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.edist_le_infEDist_add_ediam`. -/
EMetric.edist_le_infEdist_add_ediam : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
  y ∈ s → edist x y ≤ Metric.infEDist x s + Metric.ediam s
-- Lean.Data.PersistentArray
Lean.PersistentArray.div2Shift : USize → USize → USize
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- The canonical isomorphism `sheafify J (P ⋙ F) ≅ sheafify J P ⋙ F` when
`F` preserves the sheafification.  -/
CategoryTheory.sheafifyComposeIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              (F : CategoryTheory.Functor A B) →
                [inst_3 : CategoryTheory.HasWeakSheafify J A] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J B] →
                    [J.HasSheafCompose F] →
                      [J.PreservesSheafification F] →
                        (P : CategoryTheory.Functor Cᵒᵖ A) →
                          CategoryTheory.sheafify J (P.comp F) ≅ (CategoryTheory.sheafify J P).comp F
-- Mathlib.Algebra.Group.Prod
Prod.instLeftCancelMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : LeftCancelMonoid M] [inst_1 : LeftCancelMonoid N],
  Prod.instLeftCancelMonoid = { toMonoid := Prod.instMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.self_mem : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A), x ∈ StarAlgebra.elemental R x
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.mk.sizeOf_spec : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} [inst_4 : SizeOf S] [inst_5 : SizeOf C] (f : X.obj ⟶ Y.obj)
  (comm :
    autoParam
      (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) =
        CategoryTheory.CategoryStruct.comp f Y.d)
      CategoryTheory.DifferentialObject.Hom.comm._autoParam),
  sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.pathEquivList_symm_cons : ∀ {α : Type u_1} (l : List α) (a : α),
  Quiver.SingleObj.pathEquivList.symm (a :: l) = (Quiver.SingleObj.pathEquivList.symm l).cons a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.gcorec_nil : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {F : β → Option (α × γ × β)} {op : γ → Stream'.Seq α → Stream'.Seq α}
  [inst : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op] {b : β},
  F b = none → Tactic.ComputeAsymptotics.Seq.gcorec F op b = Stream'.Seq.nil
-- Mathlib.Data.DFinsupp.Notation
/-- `DFinsupp` elaborator for `update₀`.  -/
DFinsupp.Internal.elabUpdate₀ : Lean.Elab.Term.TermElab
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.insert_compl_insert : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, a ∉ s → insert a (insert a s)ᶜ = sᶜ
-- Mathlib.NumberTheory.SmoothNumbers
/-- The `n`-smooth numbers agree with the `Finset.range n`-factored numbers.  -/
Nat.smoothNumbers_eq_factoredNumbers : ∀ (n : ℕ), n.smoothNumbers = Nat.factoredNumbers (Finset.range n)
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.exists_nonneg_sub_nonneg : ∀ {R : Type u_3} [inst : AddGroup R] [inst_1 : Star R] [inst_2 : PartialOrder R] [SelfAdjointDecompose R] {a : R},
  IsSelfAdjoint a → ∃ b c, 0 ≤ b ∧ 0 ≤ c ∧ a = b - c
-- Init.Prelude
MonadReader.mk : {ρ : outParam (Type u)} → {m : Type u → Type v} → m ρ → MonadReader ρ m
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A `c : Bicone F` is:
* an object `c.pt` and
* morphisms `π j : pt ⟶ F j` and `ι j : F j ⟶ pt` for each `j`,
* such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
 -/
CategoryTheory.Limits.Bicone.ι : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → (self : CategoryTheory.Limits.Bicone F) → (j : J) → F j ⟶ self.pt
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Const.ofList l).getKey? k' = some k
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.inf_add_assoc : ∀ {G : Type u_2} [inst : AddGroup G] (A B C : AddSubgroup G), C ≤ A → ↑(A ⊓ B) + ↑C = ↑A ∩ (↑B + ↑C)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal},
  Measurable f → ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
-- Std.Time.Zoned.Database.Basic
/-- Converts a given time index into a `LocalTimeType` by using a time zone (`tz`) and its identifier.
 -/
Std.Time.TimeZone.convertLocalTimeType : ℕ → Std.Time.TimeZone.TZif.TZifV1 → String → Option Std.Time.TimeZone.LocalTimeType
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidComap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N)
  (x : ↥(AddSubmonoid.comap f N')), ↑((f.addSubmonoidComap N') x) = f ↑x
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {s : Set α} [inst_1 : NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E),
  MeasureTheory.indicatorConstLp 2 hs hμs x =
    (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (MeasureTheory.indicatorConstLp 2 hs hμs 1)
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.smulCommClass_self : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} [inst : Semiring S] [inst_1 : DistribSMul R S] [inst_2 : Add M]
  [SMulCommClass R S S], SMulCommClass R (AddMonoidAlgebra S M) (AddMonoidAlgebra S M)
-- Batteries.Data.Array.Lemmas
/-- **Alias** of `List.erase_toArray`. -/
Array.erase_toArray : ∀ {α : Type u_1} [inst : BEq α] {as : List α} {a : α}, as.toArray.erase a = (as.erase a).toArray
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of a measurable function is greater than its mean, while
avoiding a null set.  -/
MeasureTheory.exists_notMem_null_laverage_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ENNReal},
  μ ≠ 0 → ∫⁻ (a : α), f a ∂μ ≠ ⊤ → μ N = 0 → ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
-- Mathlib.MeasureTheory.Constructions.AddChar
AddChar.instMeasurableSpace : {A : Type u_1} →
  {M : Type u_2} →
    [inst : AddMonoid A] →
      [inst_1 : Monoid M] →
        [inst_2 : MeasurableSpace A] → [DiscreteMeasurableSpace A] → [Finite A] → MeasurableSpace (AddChar A M)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ext : ∀ {X Y : AddGrpCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- Given a monomorphism of sheaves `η : F ⟶ G`, an object X of the site, map an element `x : G(X)`
to the (closed) sieve on X where `f : Y → X` is in the sieve iff
  `∃ a ∈ F(Y), G(f)(x) = η_Y(a)`
 -/
CategoryTheory.Sheaf.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F G : CategoryTheory.Sheaf J (Type (max u v))} →
        (m : F ⟶ G) → [CategoryTheory.Mono m] → G ⟶ CategoryTheory.Sheaf.Ω J
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.hComp'_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {V₃ : CategoryTheory.Functor C₃ D₃}
  (E : C₂ ≌ C₃) (E' : D₂ ≌ D₃) (w' : E.functor.comp V₃ ≅ V₂.comp E'.functor) {T₁₂ : CategoryTheory.Functor C₁ C₃}
  {B₁₂ : CategoryTheory.Functor D₁ D₃} (eT : T₁.comp E.functor ≅ T₁₂) (eB : B₁.comp E'.functor ≅ B₁₂),
  (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact
-- Init.Data.AC
Lean.Data.AC.Expr : Type
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_iInf : ∀ {ι : Sort u_1} {G : Type u_2} [inst : AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.domExtend_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Bundle.Trivialization F fun z => proj ↑z)
  [inst_3 : Nonempty (Z → F)] (x : B × F),
  ↑(Bundle.Trivialization.domExtend hps e).symm x = ↑(↑e.toPretrivialization.symm x)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀_comp_H0π : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom (groupHomology.H0π A) = groupHomology.π A 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_mul_cancel : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a⁻¹ * a = 1
-- Aesop.Tree.Data
Aesop.Goal.setDepth : ℕ → Aesop.Goal → Aesop.Goal
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  (f : sInfHom β γ) (g : sInfHom α β), f.comp g = { toFun := ⇑f ∘ ⇑g, map_sInf' := ⋯ }
-- Init.System.IO
/-- Reads the entire remaining contents of the stream as a UTF-8-encoded array of lines.

Newline markers are not included in the lines.

The underlying stream is not automatically closed, and subsequent reads from the stream may block
and/or return data.
 -/
IO.FS.Stream.lines : IO.FS.Stream → IO (Array String)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.penultimate_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.penultimate = p.snd
-- Mathlib.Algebra.Order.Group.PosPart
mul_mabs_eq_oneLePart_sq : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a : α), a * |a|ₘ = a⁺ᵐ ^ 2
-- Mathlib.Dynamics.OmegaLimit
/-- **Alias** of `omegaLimit_subset_closure_image2`. -/
omegaLimit_subset_closure_fw_image : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  {u : Set τ}, u ∈ f → omegaLimit f ϕ s ⊆ closure (Set.image2 ϕ u s)
-- Aesop.Tree.TreeM
Aesop.TreeM.State.mk.sizeOf_spec : ∀ (tree : Aesop.Tree), sizeOf { tree := tree } = 1 + sizeOf tree
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instNonAssocSemiring : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonAssocSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] → [IsScalarTower R B B] → NonAssocSemiring (TensorProduct R A B)
-- Mathlib.Topology.FiberBundle.Basic
/-- The composition of two local trivializations is the trivialization change `Z.trivChange i j`.  -/
FiberBundleCore.localTrivAsPartialEquiv_trans : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i j : ι),
  (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadLift_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u} (x : m α)
  (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp x post epost.tail ⦄ MonadLift.monadLift x ⦃ post; epost ⦄
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The range of a surjective `AddSemigroup` hom is the whole of the codomain.  -/
AddHom.srange_eq_top_of_surjective : ∀ {M : Type u_1} [inst : Add M] {N : Type u_5} [inst_1 : Add N] (f : M →ₙ+ N), Function.Surjective ⇑f → f.srange = ⊤
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- For (U : Comonad C), morphisms `c ⟶ c'` in the Cokleisli category of `U` are
morphisms ` U.obj c ⟶ c'` in `C`.  -/
CategoryTheory.Cokleisli.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {U : CategoryTheory.Comonad C} → CategoryTheory.Cokleisli U → CategoryTheory.Cokleisli U → Type v
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.symm_mapAlgEquiv : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (e : A ≃ₐ[R] B),
  (MonoidAlgebra.mapAlgEquiv R M e).symm = MonoidAlgebra.mapAlgEquiv R M e.symm
-- Mathlib.Condensed.TopComparison
/-- `TopCat.toSheafCompHausLike` yields a functor from `TopCat.{max u w}` to
`Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w))`.
 -/
topCatToSheafCompHausLike : (P : TopCat → Prop) →
  [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
    [inst_1 : CompHausLike.HasExplicitPullbacks P] →
      (hs :
          ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
            CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
        have this := ⋯;
        CategoryTheory.Functor TopCat
          (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_pos_of_orderOf_pos : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M},
  0 < orderOf m → ∀ (a : α), 0 < MulAction.period m a