mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.integral_llr_tilted_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ →
      MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
        MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
          ∫ (x : α), MeasureTheory.llr μ (ν.tilted f) x ∂μ =
            ∫ (x : α), MeasureTheory.llr μ ν x ∂μ - ∫ (x : α), f x ∂μ + Real.log (∫ (x : α), Real.exp (f x) ∂ν)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List α} {k k' : α},
  (k == k') = true → k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).get! k' = k
-- Mathlib.RingTheory.Ideal.Prod
Ideal.isPrime_of_isPrime_prod_top : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R}, (I.prod ⊤).IsPrime → I.IsPrime
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.keys : Lean.Meta.SimpTheorem → Array Lean.Meta.SimpTheoremKey
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- The `qc`-precoverage of a scheme wrt. to a morphism property `P` is the precoverage
given by quasi-compact covers satisfying `P`.  -/
AlgebraicGeometry.Scheme.propQCPrecoverage : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_1 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.move p k₁ k₂ q with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_1 p k₁ k₂ q
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Given a `2`-truncated simplicial set `X` and a category `C`,
this is the functor `X.HomotopyCategory ⥤ C` corresponding to
a morphism `X ⟶ (truncation 2).obj (nerve C)`.  -/
SSet.Truncated.HomotopyCategory.descOfTruncation : {X : SSet.Truncated 2} →
  {C : Type u} →
    [inst : CategoryTheory.SmallCategory C] →
      (X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C)) → CategoryTheory.Functor X.HomotopyCategory C
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `Nat.card_zpowers`.  -/
Fintype.card_zpowers : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, Fintype.card ↥(Subgroup.zpowers x) = orderOf x
-- Mathlib.RingTheory.Derivation.Lie
/-- The commutator of derivations is again a derivation.  -/
Derivation.instBracket : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → Bracket (Derivation R A A) (Derivation R A A)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_pos_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, 0 < Metric.coveringNumber ε A ↔ A.Nonempty
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_getKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} (h' : a ∈ t), t.getKey? a = some (t.getKey a h')
-- Std.Net.Addr
/-- Turn `addr` into a `String` in the usual IPv4 format.
 -/
Std.Net.IPv4Addr.toString : Std.Net.IPv4Addr → String
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- If `F.op` is triangulated, so is `F`.
 -/
CategoryTheory.Functor.isTriangulated_of_op : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_8 : CategoryTheory.Pretriangulated C]
  [inst_9 : CategoryTheory.Limits.HasZeroObject D] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  [F.op.IsTriangulated], F.IsTriangulated
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrp_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided] (A : CategoryTheory.CommGrp C),
  (F.mapCommGrp.obj A).X = F.obj A.X
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eq_biInf : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l = ⨅ i, ⨅ (_ : p i), Filter.principal (s i)
-- Mathlib.Data.PNat.Prime
/-- The least common multiple (lcm) of two positive natural numbers,
viewed as positive natural number.  -/
PNat.lcm : ℕ+ → ℕ+ → ℕ+
-- Lean.DocString.Markdown
/-- Runs a Markdown-rendering action against an environment, building a minimal `CoreM` context.
 -/
Lean.Doc.runMarkdown : {α : Type} →
  Lean.Environment →
    Lean.CoreM α →
      optParam Lean.Options ∅ →
        optParam Lean.Name Lean.Name.anonymous →
          optParam (List Lean.OpenDecl) [] → optParam (Option IO.CancelToken) none → IO α
-- Init.Data.UInt.Basic
/-- Bitwise complement, also known as bitwise negation, for word-sized unsigned integers. Usually
accessed via the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.
 -/
USize.complement : USize → USize
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_cons : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : G) (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u)
  (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
  HNNExtension.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.cons g u w h1 h2).toReducedWord =
    HNNExtension.of g * (HNNExtension.t ^ ↑u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord)
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_right : ∀ (m n : ℕ), n.gcd (n * m) = n
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
/-- The Clifford algebra over an orthogonal direct sum of quadratic vector spaces is isomorphic
as an algebra to the graded tensor product of the Clifford algebras of each space.

This is `CliffordAlgebra.toProd` and `CliffordAlgebra.ofProd` as an equivalence.  -/
CliffordAlgebra.prodEquiv : {R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                (Q₁ : QuadraticForm R M₁) →
                  (Q₂ : QuadraticForm R M₂) →
                    CliffordAlgebra (QuadraticMap.prod Q₁ Q₂) ≃ₐ[R]
                      GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is a sheaf for the sieve `S` on `X`, a natural transformation from `S` (viewed as a functor)
to `P` can be (uniquely) extended to all of `yoneda.obj X`.
```
      f
   S  →  P
   ↓  ↗
   yX
```
 -/
CategoryTheory.Presieve.IsSheafFor.extend : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Sieve X} →
        {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
          CategoryTheory.Presieve.IsSheafFor P S.arrows → (S.functor ⟶ P) → (CategoryTheory.yoneda.obj X ⟶ P)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.big_intersection : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} {a b : G},
  a ∈ B → b ∈ B → 2 * A.card ≤ (a • A ∩ b • A).card + (B * A).card
-- Mathlib.Data.Nat.Nth
Nat.nth_zero_of_exists : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), Nat.nth p 0 = Nat.find h
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.rightUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (P : C),
  (CategoryTheory.Limits.coprod.rightUnitor P).hom =
    CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id P) (CategoryTheory.Limits.initial.to P)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.loopless : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), Std.Irrefl G'.Adj
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.List.mapFinIdx.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (as : List α)
  (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) (acc : Array β)
  (h : [].length + acc.size = as.length)
  (h_1 : (acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h)
  (h_2 :
    (a : α) →
      (as_1 : List α) → (acc : Array β) → (h : (a :: as_1).length + acc.size = as.length) → motive (a :: as_1) acc h),
  (match [], acc, h with
    | [], acc, h => h_1 acc h
    | a :: as_1, acc, h => h_2 a as_1 acc h) =
    h_1 acc h
-- Mathlib.Algebra.Ring.BooleanRing
RingEquiv.asBoolRingAsBoolAlg_symm_apply : ∀ (α : Type u_4) [inst : BooleanRing α] (a : α), (RingEquiv.asBoolRingAsBoolAlg α).symm a = toBoolRing (toBoolAlg a)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_subsingleton : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R),
  A.updateCol i b = (Matrix.replicateCol (Fin 1) b).submatrix id (Function.const n 0)
-- Lean.Parser.Term
Lean.Parser.Term.letOptGeneralize.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_toFinset : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] (l : List α) (f : α → β)
  (comm : (↑l.toFinset).Pairwise (Function.onFun AddCommute f)),
  l.Nodup → l.toFinset.noncommSum f comm = (List.map f l).sum
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_empty : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m : MeasureTheory.AddContent G C}, m ∅ = 0
-- Mathlib.FieldTheory.AbelRuffini
/-- **Alias** of `isSolvable_gal_minpoly`. -/
solvableByRad.isSolvable : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E → Group.IsSolvable (minpoly F x).Gal
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoMod hp (a - ↑m * p) b = toIcoMod hp a b - ↑m * p
-- Mathlib.Data.Set.Order
Monotone.union : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α},
  Monotone f → Monotone g → Monotone fun x => f x ∪ g x
-- Init.Data.Array.InsertIdx
Array.size_insertIdx : ∀ {α : Type u} {a : α} {i : ℕ} {xs : Array α} (h : i ≤ xs.size), (xs.insertIdx i a h).size = xs.size + 1
-- Mathlib.CategoryTheory.Widesubcategory
/-- The forgetful functor from a wide subcategory into the original category
("forgetting" the condition).
 -/
CategoryTheory.wideSubcategoryInclusion : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : P.IsMultiplicative] → CategoryTheory.Functor (CategoryTheory.WideSubcategory P) C
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.ordConnected_setOfPred_eball_subset`. -/
EMetric.ordConnected_setOf_ball_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), {r | Metric.eball x r ⊆ s}.OrdConnected
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList.match_1.congr_eq_2 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord M x x_1)
  (h_1 : (i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a))
  (h_2 :
    (x x_3 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord M x j) →
        (_hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_3) → motive x x_3 (w₁.append _hne w₂))
  (x_3 x_4 j k : ι) (w₁ : Monoid.CoprodI.NeWord M x_3 j) (_hne : j ≠ k) (w₂ : Monoid.CoprodI.NeWord M k x_4),
  x = x_3 →
    x_1 = x_4 →
      x_2 ≍ w₁.append _hne w₂ →
        (match x, x_1, x_2 with
          | i, .(i), Monoid.CoprodI.NeWord.singleton x a => h_1 i x a
          | x, x_5, w₁.append _hne w₂ => h_2 x x_5 j k w₁ _hne w₂) ≍
          h_2 x_3 x_4 j k w₁ _hne w₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.cosh` is real analytic.  -/
Real.analyticAt_cosh : ∀ {x : ℝ}, AnalyticAt ℝ Real.cosh x
-- Mathlib.Data.Int.Associated
Int.natAbs_eq_iff_associated : ∀ {a b : ℤ}, a.natAbs = b.natAbs ↔ Associated a b
-- Mathlib.Order.Filter.Ultrafilter.Basic
/-- The ultrafilter extending the cofinite filter.  -/
Filter.hyperfilter : (α : Type u) → [Infinite α] → Ultrafilter α
-- Lean.Exception
/-- Like `mkUnknownIdentifierMessage`, but does not tag the message.  -/
Lean.mkUnknownIdentifierMessageCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadError m] → Lean.MessageData → optParam Lean.Name Lean.Name.anonymous → m Lean.MessageData
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} {t₁ t₂ : Multiset β},
  s₁ ≤ s₂ → t₁ ≤ t₂ → s₁.disjSum t₁ ≤ s₂.disjSum t₂
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instGroupWithZero : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → GroupWithZero (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] →
                      GroupWithZero (DirectLimit G f)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitBackward.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C)
  (x : F.obj (Opposite.op X)),
  CategoryTheory.OverPresheafAux.unitBackward η X x =
    CategoryTheory.OverPresheafAux.YonedaCollection.mk
      (CategoryTheory.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op X))) x)) ⟨x, ⋯⟩
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an `AddZeroClass`, if it admits a
surjective map that preserves `0` and `+` to an `AddZeroClass`.  -/
Function.Surjective.addZeroClass : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : Zero M₂] →
        [inst_2 : AddZeroClass M₁] →
          (f : M₁ → M₂) → Function.Surjective f → f 0 = 0 → (∀ (x y : M₁), f (x + y) = f x + f y) → AddZeroClass M₂
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instLeast? : Std.PRange.Least? ISize
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.toCycles_comp_isoCycles₂_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupHomology.cycles₂ A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.toCycles A 3 2)
      (CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.f' h)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_7.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_8 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t
-- Mathlib.Data.LawfulXor.Equiv
Equiv.xor_involutive : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α] (a : α), Function.Involutive ⇑(Equiv.xor a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.cast_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {a : R}, Mathlib.Meta.NormNum.IsNat a 0 → a = 0
-- Mathlib.RingTheory.Valuation.RankOne
ValuativeRel.isNontrivial_of_rankOne : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [h : (ValuativeRel.valuation R).RankOne],
  ValuativeRel.IsNontrivial R
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eval_eq_prod_roots_of_monic : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f.Monic → ∀ (x : R), Polynomial.eval x f = (Multiset.map (fun x_1 => x - x_1) f.roots).prod
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.Composition.recOnSingleAppend.match_1.eq_1 : ∀ (motive : (blocks : List ℕ) → (∀ {i : ℕ}, i ∈ blocks → 0 < i) → Sort u_1) (blocks_pos : ∀ {i : ℕ}, i ∈ [] → 0 < i)
  (h_1 : (blocks_pos : ∀ {i : ℕ}, i ∈ [] → 0 < i) → motive [] blocks_pos)
  (h_2 : (tail : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail → 0 < i) → motive (0 :: tail) blocks_pos)
  (h_3 : (k : ℕ) → (l : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i) → motive (k.succ :: l) blocks_pos),
  (match [], blocks_pos with
    | [], blocks_pos => h_1 blocks_pos
    | 0 :: tail, blocks_pos => h_2 tail blocks_pos
    | k.succ :: l, blocks_pos => h_3 k l blocks_pos) =
    h_1 blocks_pos
-- Mathlib.Algebra.Lie.Ideal
LieHom.idealRange_eq_lieSpan_range : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'),
  f.idealRange = LieSubmodule.lieSpan R L' ↑f.range
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The positive cone of an ordered module is always salient.  -/
ConvexCone.salient_positive : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] {G : Type u_7} [inst_2 : AddCommGroup G]
  [inst_3 : PartialOrder G] [inst_4 : IsOrderedAddMonoid G] [inst_5 : Module R G] [inst_6 : PosSMulMono R G],
  (ConvexCone.positive R G).Salient
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.biSup_iInf_eq : ∀ {α : Type u} {ι : Type v} {κ : ι → Sort w} [Nonempty ((a : ι) → κ a)] [inst : Order.Coframe α] {s : Set ι},
  s.Finite → ∀ {f : (a : ι) → κ a → α}, ⨆ a ∈ s, ⨅ b, f a b = ⨅ g, ⨆ a ∈ s, f a (g a)