mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- A component of the natural transformation between left-derived functors can be computed
using a chosen projective resolution.  -/
CategoryTheory.ProjectiveResolution.leftDerived_app_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) (n : ℕ),
  (CategoryTheory.NatTrans.leftDerived α n).app X =
    CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex))
        (P.isoLeftDerivedObj G n).inv)
-- Mathlib.Algebra.Star.Unitary
Unitary.instMulActionSubtypeMemSubmonoidUnitary : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : Monoid A] →
        [inst_2 : MulAction R A] →
          [SMulCommClass R A A] →
            [IsScalarTower R A A] →
              [inst_5 : StarMul R] → [inst_6 : StarMul A] → [StarModule R A] → MulAction ↥(unitary R) ↥(unitary A)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Convert an `rintro` pattern to an equivalent `intro` argument, if possible.  -/
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.introMergeArgOfRIntroPat? : Lean.TSyntax `rintroPat → Option Lean.Term
-- Mathlib.Algebra.Group.Prod
MulEquiv.coe_prodAssoc_symm : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P],
  ⇑MulEquiv.prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.instUniqueQuotientTop : {R : Type u_3} → [inst : Ring R] → Unique (R ⧸ ⊤)
-- Std.Data.HashSet.Basic
Std.HashSet.instSingleton : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Singleton α (Std.HashSet α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.strictMonoOn_tan : StrictMonoOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
-- Lean.Parser.Syntax
Lean.Parser.Command.macro_rules : Lean.Parser.Parser
-- Init.Data.Array.Sort.Lemmas
/-- Another statement of stability of merge sort.
If a pair `[a, b]` is a sublist of `xs.toList` and `le a b`,
then `[a, b]` is still a sublist of `(mergeSort le xs).toList`.
 -/
Array.pair_sublist_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {a b : α} {xs : Array α},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      le a b = true → [a, b].Sublist xs.toList → [a, b].Sublist (xs.mergeSort le).toList
-- Mathlib.CategoryTheory.Functor.Flat
/-- (Implementation).
Given a limit cone `c : cone K` and a cone `s : cone (K ⋙ F)` with `F` representably flat,
`s` can factor through `F.mapCone c`.
 -/
CategoryTheory.PreservesFiniteLimitsOfFlat.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type v₁} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            [CategoryTheory.FinCategory J] →
              {K : CategoryTheory.Functor J C} →
                (F : CategoryTheory.Functor C D) →
                  [CategoryTheory.RepresentablyFlat F] →
                    {c : CategoryTheory.Limits.Cone K} →
                      CategoryTheory.Limits.IsLimit c → (s : CategoryTheory.Limits.Cone (K.comp F)) → s.pt ⟶ F.obj c.pt
-- Mathlib.Algebra.Order.Group.Action
smul_strictMono_right : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : Preorder α] [CovariantClass M α HSMul.hSMul LT.lt] (m : M),
  StrictMono (HSMul.hSMul m)
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_dvd_iff_forall_pow_eq_one : ∀ {G : Type u} [inst : Monoid G] {n : ℕ}, Monoid.exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.codRestrict_toMultilinearMap : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p),
  (f.codRestrict p h).toMultilinearMap = f.codRestrict p h
-- Std.Data.TreeMap.Lemmas
_private.Std.Data.TreeMap.Lemmas.0.Std.TreeMap.equiv_iff_equiv : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ ↔ t₁.inner.Equiv t₂.inner
-- Mathlib.Algebra.Group.Irreducible.Defs
/-- `AddIrreducible p` states that `p` is not an additive unit and cannot be written as a sum of
additive non-units. 

[Wikidata Q2989575](https://www.wikidata.org/wiki/Q2989575) -/
AddIrreducible : {M : Type u_1} → [AddMonoid M] → M → Prop
-- Mathlib.Data.List.Basic
List.cons_head?_tail : ∀ {α : Type u} {l : List α} {a : α}, a ∈ l.head? → a :: l.tail = l
-- Mathlib.Topology.Order.NhdsSet
Ici_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  a < b → Set.Ici a ∈ nhdsSet (Set.Icc b c)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.linearMap_qext_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f g : M ⧸ p →ₛₗ[τ₁₂] M₂}, f = g ↔ f ∘ₛₗ p.mkQ = g ∘ₛₗ p.mkQ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.equivOfIsoObj_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (e : Y ≅ X) (R : F.RepresentableBy X), (CategoryTheory.Functor.RepresentableBy.equivOfIsoObj e) R = R.ofIsoObj e
-- Init.Data.Array.Find
Array.get_find?_mem : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} (h : (Array.find? p xs).isSome = true), (Array.find? p xs).get h ∈ xs
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Two multiplicative isomorphisms agree if they are defined by the
same underlying function.  -/
MulEquiv.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M ≃* N}, (∀ (x : M), f x = g x) → f = g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t₁ ∪ t₂).getKey! k = t₂.getKeyD k (t₁.getKey! k)
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.basisMatrix.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a a_1 : K →+* ℂ),
  a = a_1 → ∀ (a_2 a_3 : K →+* ℂ), a_2 = a_3 → NumberField.basisMatrix K a a_2 = NumberField.basisMatrix K a_1 a_3
-- Lean.Parser.Command
Lean.Parser.Command.recommended_spelling.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_hsum_eq_sum_of_subset : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α} {g : Γ} {t : Finset α},
  {a | (s a).coeff g ≠ 0} ⊆ ↑t → s.hsum.coeff g = ∑ i ∈ t, (s i).coeff g
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.one_right : ∀ (a : ℕ), Mathlib.Meta.NormNum.jacobiSymNat a 1 = 1
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.surjective_respectsIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  (CategoryTheory.MorphismProperty.surjective C).RespectsIso
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notDefEq.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- Forgets the third fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₃.forgetThd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → W.LeftFraction₂ X Y
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.mul_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  (∀ i ∈ s, 0 ≤ g₁ i) → (∀ i ∈ s, 0 ≤ g₂ i) → AntivaryOn f g₁ s → AntivaryOn f g₂ s → AntivaryOn f (g₁ * g₂) s
-- Init.Core
Quot.indepCoherent : ∀ {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (Quot.mk r a)),
  (∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) → ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mul_bot : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), I * ⊥ = ⊥
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_2_comp_chainsIso₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 2) (groupHomology.chainsIso₂ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).hom (groupHomology.chainsMap₂ f φ)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.refl_toLinearMap : ∀ {R : Type u_1} {M : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(LinearEquiv.refl R M) = LinearMap.id
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometry.inr_apply : ∀ (𝕜 : Type u_9) [inst : NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (y : F),
  (LinearIsometry.inr 𝕜 E F) y = (0, y)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TheoremGuard.mk.sizeOf_spec : ∀ (e : Lean.Expr) (check : Bool), sizeOf { e := e, check := check } = 1 + sizeOf e + sizeOf check
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Measurable equivalence between (dependent) functions on a type and pairs of functions on
`{i // p i}` and `{i // ¬p i}`. See also `Equiv.piEquivPiSubtypeProd`.  -/
MeasurableEquiv.piEquivPiSubtypeProd : {δ' : Type u_5} →
  (π : δ' → Type u_6) →
    [inst : (x : δ') → MeasurableSpace (π x)] →
      (p : δ' → Prop) → [DecidablePred p] → ((i : δ') → π i) ≃ᵐ ((i : Subtype p) → π ↑i) × ((i : { i // ¬p i }) → π ↑i)
-- Mathlib.RingTheory.Congruence.Basic
/-- For congruence relations `c, d` on a type `M` with multiplication and addition, `c ≤ d` iff
`∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`.  -/
RingCon.instLE : {R : Type u_3} → [inst : Add R] → [inst_1 : Mul R] → LE (RingCon R)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R X : C} {p₁ p₂ : R ⟶ X}
  {toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂} {c : CategoryTheory.Limits.PullbackCone p₂ p₁}
  {isLimit : CategoryTheory.Limits.IsLimit c} {t : c.pt ⟶ R}
  {transitivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam}
  {transitivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam}
  {toJointlyMono₂_1 : CategoryTheory.JointlyMono₂ p₁ p₂} {c_1 : CategoryTheory.Limits.PullbackCone p₂ p₁}
  {isLimit_1 : CategoryTheory.Limits.IsLimit c_1} {t_1 : c_1.pt ⟶ R}
  {transitivity₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₁ = CategoryTheory.CategoryStruct.comp c_1.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam}
  {transitivity₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₂ = CategoryTheory.CategoryStruct.comp c_1.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam},
  { toJointlyMono₂ := toJointlyMono₂, c := c, isLimit := isLimit, t := t, transitivity₁ := transitivity₁,
        transitivity₂ := transitivity₂ } =
      { toJointlyMono₂ := toJointlyMono₂_1, c := c_1, isLimit := isLimit_1, t := t_1, transitivity₁ := transitivity₁_1,
        transitivity₂ := transitivity₂_1 } →
    c = c_1 ∧ isLimit ≍ isLimit_1 ∧ t ≍ t_1
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Client.mk : Std.Http.Internal.Mock.SharedState✝ → Std.Http.Internal.Mock.Client
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.cechConerve_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  {x y : SimplexCategory} (g : x ⟶ y),
  f.cechConerve.map g =
    CategoryTheory.Limits.WidePushout.desc (CategoryTheory.Limits.WidePushout.head fun x => f.hom)
      (fun i => CategoryTheory.Limits.WidePushout.ι (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g) i)) ⋯
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.TotalSpace.toProd.eq_1 : ∀ (B : Type u_4) (F : Type u_5),
  Bundle.TotalSpace.toProd B F =
    { toFun := fun x => (x.proj, x.snd), invFun := fun x => ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The function that sends `x` to the `y`-derivative of `f(x,y)` at `g(x)` applied to `g₂(x)` is
`C^n` at `x₀`, where the derivative is taken as a continuous linear map.
We have to assume that `f` is `C^(n+1)` at `(x₀, g(x₀))` and `g` is `C^n` at `x₀`.
We have to insert a coordinate change from `x₀` to `g₁(x)` to make the derivative sensible.

This is similar to `ContMDiffAt.mfderiv`, but where the continuous linear map is applied to a
(variable) vector.
 -/
ContMDiffAt.mfderiv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  [Js : IsManifold J 1 N] {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F']
  {G' : Type u_12} [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13}
  [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M']
  {x₀ : N'} (f : N → M → M') (g : N → M) (g₁ : N' → N) (g₂ : N' → E),
  ContMDiffAt (J.prod I) I' n (Function.uncurry f) (g₁ x₀, g (g₁ x₀)) →
    ContMDiffAt J I m g (g₁ x₀) → ContMDiffAt J' J m g₁ x₀ → ⋯ → ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
Measurable.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α → β),
  Measurable f = ∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (f ⁻¹' t)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuousOn_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {s : Set β},
  ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
-- Mathlib.Algebra.Group.Equiv.Defs
/-- A multiplicative isomorphism preserves multiplication.  -/
MulEquiv.map_mul : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (x y : M), f (x * y) = f x * f y
-- Init.Data.Nat.Lemmas
Nat.eq_div_iff_mul_eq_left : ∀ {c b a : ℕ}, c ≠ 0 → c ∣ b → (a = b / c ↔ b = a * c)
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_bot_le_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrderBot ι] [WellFoundedLT ι]
  {u : ι → Ω → β} {s : Set β} {i : ι} {ω : Ω}, MeasureTheory.hittingAfter u s ⊥ ω ≤ ↑i ↔ ∃ j ≤ i, u j ω ∈ s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology.cocycles A 2)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesMap f φ 2)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ f φ))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ A).hom) x)
-- Init.Data.SInt.Lemmas
Int64.ne_iff_ofBitVec_ne : ∀ {a b : BitVec 64}, a ≠ b ↔ Int64.ofBitVec a ≠ Int64.ofBitVec b
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_eq_zero_of_left : ∀ {M₀ : Type u_2} {A : Type u_7} [inst : Zero M₀] [inst_1 : Zero A] [inst_2 : SMulWithZero M₀ A] {a : M₀},
  a = 0 → ∀ (b : A), a • b = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P ≈ Q
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool},
  (Std.ExtDTreeMap.filter (fun k x => f k) t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = true
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.getArity : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → ℕ
-- Batteries.Recycling.RBTree.Basic
/-- A red node is required to have black children.  -/
RBTree.RBColor.red : RBTree.RBColor
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp),
  CategoryTheory.Limits.coconeLeftOpOfConeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coneOfCoconeLeftOp c)
-- Mathlib.Data.Holor
/-- `HolorIndex ds` is the type of valid index tuples used to identify an entry of a holor
of dimensions `ds`.  -/
HolorIndex : List ℕ → Type
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.isPlotOn_reparam : ∀ {X : Type u_1} (self : DiffeologicalSpace.CorePlotsOn X) {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))}
  {v : Set (EuclideanSpace ℝ (Fin m))} {hu : IsOpen u} (hv : IsOpen v) {p : EuclideanSpace ℝ (Fin n) → X}
  {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
  Set.MapsTo f v u → self.isPlotOn hu p → ContDiffOn ℝ (↑⊤) f v → self.isPlotOn hv (p ∘ f)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_apply_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) {x : N} {y : M}, e.symm x = y ↔ x = e y
-- Mathlib.Logic.Basic
imp_forall_iff_forall : ∀ (A : Prop) (B : A → Prop), (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Isomorphic presheaves have isomorphic sheaf condition diagrams.  -/
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        {F : TopCat.Presheaf C X} →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              {G : TopCat.Presheaf C X} →
                (F ≅ G) →
                  (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U ≅
                    TopCat.Presheaf.SheafConditionEqualizerProducts.diagram G U)
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidates.report : Lean.Elab.Structural.RecArgCandidates → Lean.MessageData
-- Lean.Meta.HaveTelescope
/-- The proof that the simplified expression is equal to the input one.
It may contain loose bound variables like in the `expr` field.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.proof : Lean.Meta.SimpHaveResult✝ → Lean.Expr
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_7 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId)
  (cidx : ℕ) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_7 fvarId cidx h
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instSMulPosReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : DistribMulAction α β] [SMulPosReflectLE α β],
  SMulPosReflectLE α βᵒᵈ