mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Rel.GaloisConnection
SetRel.leftDual_rightDual_le_of_le : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) {I I' : Set β},
  I' ∈ R.rightFixedPoints → I ⊆ I' → R.leftDual (R.rightDual I) ⊆ I'
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_le_netEntropyEntourage : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X),
  Dynamics.netEntropyInfEntourage T F U ≤ Dynamics.netEntropyEntourage T F U
-- Mathlib.Data.Multiset.Defs
/-- "Attach" a proof that `a ∈ s` to each element `a` in `s` to produce
a multiset on `{x // x ∈ s}`.  -/
Multiset.attach : {α : Type u_1} → (s : Multiset α) → Multiset { x // x ∈ s }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Sequence.mk.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] (elems' elems'_1 : ℕ → Polynomial R) (e_elems' : elems' = elems'_1)
  (degree_eq' : ∀ (i : ℕ), (elems' i).degree = ↑i),
  { elems' := elems', degree_eq' := degree_eq' } = { elems' := elems'_1, degree_eq' := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `M` is a flat `R`-module, then for any family of
`R`-linearly independent elements `{ n_i }` of `N`, they are also `M`-linearly independent,
in the sense that the `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }`
to the sum of `m_i * n_i` (`Submodule.mulRightMap M n`) has trivial kernel.  -/
Submodule.LinearDisjoint.linearIndependent_right_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Module.Flat R ↥M] {ι : Type u_1} {n : ι → ↥N}, LinearIndependent R n → (M.mulRightMap n).ker = ⊥
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.instMulActionMulActionHomIdOfSMulCommClass : {M : Type u_1} →
  {α : Type u_2} →
    {N : Type u_3} →
      {β : Type u_4} →
        [inst : Monoid M] →
          [inst_1 : MulAction M α] →
            [inst_2 : SMul N α] → [SMulCommClass M N α] → [inst_4 : SMul N β] → MulAction Mᵈᵐᵃ (α →ₑ[id] β)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_σ_self' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    CategoryTheory.CategoryStruct.comp (X.δ j) (X.σ i) = CategoryTheory.CategoryStruct.id (X.obj { len := n })
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- **Alias** of `MeasureTheory.Measure.nullSingletonClass_hausdorff`. -/
MeasureTheory.Measure.noAtoms_hausdorff : ∀ (X : Type u_2) [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ},
  0 < d → MeasureTheory.NullSingletonClass (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.Order.SymmDiff
bihimp_right_inj : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, bihimp a b = bihimp a c ↔ b = c
-- Init.Data.List.Count
List.Sublist.countP_le : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₁.Sublist l₂ → List.countP p l₁ ≤ List.countP p l₂
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuousAt_lift₂ : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z}
  {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {x : X} {y : Y},
  ContinuousAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔
    ContinuousAt (Function.uncurry f) (x, y)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_snd_v'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (n : ℤ) {Z : C}
  (h : G.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (n - 1) n)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v n n ⋯) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (n - 1) n ⋯) (φ.f n) +
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v (n - 1) (n - 1) ⋯) (G.d (n - 1) n))
      h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f)
            (CategoryTheory.Over.mk gA) (CategoryTheory.Over.mk gB)).inv)
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst gA gB) gA) f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gA)).hom
        ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk gB)).hom)
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Over.mk gB).hom f)
-- Mathlib.Topology.Defs.Filter
/-- The filter of neighborhoods of a set in a topological space.  -/
Topology.«term𝓝ˢ» : Lean.ParserDescr
-- Lean.Server.Requests
Lean.Server.RequestM.checkCancelled : Lean.Server.RequestM Unit
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_3 : ∀ (motive : Lean.Expr → Sort u_1) (deBruijnIndex : ℕ) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.bvar deBruijnIndex with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | e => h_7 e) =
    h_3 deBruijnIndex
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.mk : {α : Type u_4} →
  (Has : Set α → Prop) →
    Has ∅ →
      (∀ {a : Set α}, Has a → Has aᶜ) →
        (∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)) →
          MeasurableSpace.DynkinSystem α
-- Mathlib.Tactic.Translate.GuessName
/-- Register a new `GuessNameExt`.  -/
Mathlib.Tactic.GuessName.registerGuessNameExt : Mathlib.Tactic.GuessName.GuessNameData → IO Mathlib.Tactic.GuessName.GuessNameExt
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.comap_le_comap_iff_of_le_range : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  {f : M →ₛₗ[σ₁₂] M₂} [inst_6 : RingHomSurjective σ₁₂] {p q : Submodule R₂ M₂},
  p ≤ f.range → (Submodule.comap f p ≤ Submodule.comap f q ↔ p ≤ q)
-- Mathlib.Order.Heyting.Basic
Codisjoint.himp_inf_cancel_right : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → b ⇨ a ⊓ b = a
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciSup_iff' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {s : ι → α} {a : α},
  BddAbove (Set.range s) → (a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.wait : {α : Type} → Lean.Server.ServerTask α → BaseIO α
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel_empty : ∀ {α : Type u_1} {β : Type u_2} {r : α → β}, Std.Sat.CNF.relabel r Std.Sat.CNF.empty = Std.Sat.CNF.empty
-- Mathlib.Algebra.Order.Archimedean.Class
/-- 0 is in its own class (see `ArchimedeanClass.mk_eq_top_iff`),
which is also the largest class.  -/
ArchimedeanClass.instOrderTop : {M : Type u_1} →
  [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → OrderTop (ArchimedeanClass M)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mul_sumInl_toMatrix_prod : ∀ {n : Type u_1} (p : Type u_2) {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (M : Matrix n n R) (L : List (Matrix.TransvectionStruct n R))
  (N : Matrix p p R),
  Matrix.fromBlocks M 0 0 N *
      (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod =
    Matrix.fromBlocks (M * (List.map Matrix.TransvectionStruct.toMatrix L).prod) 0 0 N
-- Mathlib.Algebra.Order.Group.Equiv
toEquiv_ofLexAddEquiv : ∀ (α : Type u_1) [inst : Add α], ↑(ofLexAddEquiv α) = ofLex
-- Mathlib.RingTheory.Trace.Basic
Algebra.embeddingsMatrix_apply : ∀ {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : CommRing C] [inst_4 : Algebra A C] (b : κ → B) (i : κ) (σ : B →ₐ[A] C),
  Algebra.embeddingsMatrix A C b i σ = σ (b i)
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.diag` as a `LinearMap`.  -/
Matrix.diagLinearMap : (n : Type u_3) →
  (R : Type u_7) →
    (α : Type u_11) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → Matrix n n α →ₗ[R] n → α
-- Lean.Elab.Tactic.Induction
/-- Returns true if the `Lean.Parser.Tactic.inductionAlt` either has more than one alternative
or has no RHS.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.shouldExpandAlt : Lean.Syntax → Bool
-- Mathlib.LinearAlgebra.Prod
LinearMap.ker_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃), (f.prod g).ker = f.ker ⊓ g.ker
-- Init.Data.Array.Lemmas
List.foldlM_push_eq_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α} {f : α → m β}
  {xs : Array β},
  List.foldlM (fun xs x => xs.push <$> f x) xs l = do
    let __do_lift ← List.mapM f l
    pure (xs ++ __do_lift.toArray)
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.to_normOneClass : ∀ {α : Type u_2} [inst : NormedDivisionRing α], NormOneClass α
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals the real derivative.
 -/
complexOfReal_deriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ},
  DifferentiableAt ℝ f x → (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1 → deriv f x = (fderiv ℝ f x) 1
-- Batteries.CodeAction.Attr
/-- A tactic code action extension.  -/
Batteries.CodeAction.TacticCodeAction : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictFDerivAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) • f') x
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.coe_ne_zero : ∀ {α : Type u} {a : α}, ↑a ≠ 0
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.nontrivial_iff : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R}, Nontrivial (R ⧸ I) ↔ I ≠ ⊤
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedStats.default : Lean.Meta.Simp.Stats
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The `n`-independent sets in a graph as a finset.  -/
SimpleGraph.indepSetFinset : {α : Type u_1} → (G : SimpleGraph α) → [Fintype α] → [DecidableEq α] → [DecidableRel G.Adj] → ℕ → Finset (Finset α)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.CountableAB4.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCountableCoproducts C],
  (∀ (α : Type) [inst_2 : Countable α], CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C) →
    CategoryTheory.CountableAB4 C
-- Mathlib.Order.Hom.Lex
Prod.Lex.sumLexProdLexDistrib_symm_apply : ∀ (α : Type u_4) (β : Type u_5) (γ : Type u_6) [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (a : Lex (α × γ) ⊕ₗ Lex (β × γ)),
  (RelIso.symm (Prod.Lex.sumLexProdLexDistrib α β γ)) a =
    toLex (Prod.map (⇑toLex) id ((Equiv.sumProdDistrib α β γ).symm (Sum.map (⇑ofLex) (⇑ofLex) (ofLex a))))
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instCoeAddSubgroup.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenNormalAddSubgroup.instCoeAddSubgroup = { coe := fun H => ↑H.toOpenAddSubgroup }
-- Lean.Meta.HaveTelescope
Lean.Meta.instInhabitedHaveInfo : Inhabited Lean.Meta.HaveInfo
-- Mathlib.FieldTheory.Galois.Basic
AlgEquiv.transfer_galois : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] {E' : Type u_4} [inst_2 : Field E']
  [inst_3 : Algebra F E'] [inst_4 : Algebra F E] (f : E ≃ₐ[F] E'), IsGalois F E ↔ IsGalois F E'
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec.repr.match_1.splitter : (motive : Lean.Doc.ArgSpec✝ → Sort u_1) →
  (x : Lean.Doc.ArgSpec✝) →
    ((a : Lean.Name) → (a_1 : Lean.Expr) → motive (Lean.Doc.ArgSpec.positional✝ a a_1)) →
      ((a : Lean.Name) → (a_1 a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.named✝ a a_1 a_2)) →
        ((a : Lean.Name) → (a_1 : Lean.Expr) → motive (Lean.Doc.ArgSpec.many✝ a a_1)) →
          ((a : Lean.Name) → (a_1 : Bool) → motive (Lean.Doc.ArgSpec.flag✝ a a_1)) → motive x
-- Mathlib.Combinatorics.Matroid.Loop
/-- The loopless matroid obtained from `M` by deleting all its loops.  -/
Matroid.removeLoops : {α : Type u_1} → Matroid α → Matroid α
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.just_loogle_tactic : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- `colim Dᵢ` is the pullback of the glued object over `S` along the inclusion `𝒰ᵢ ⟶ S`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                      [inst_5 :
                          ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                            CategoryTheory.Limits.PreservesColimitsOfShape J
                              (CategoryTheory.MorphismProperty.Over.pullback P ⊤
                                (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))] →
                        [inst_6 : Quiver.IsThin 𝒰.I₀] →
                          [inst_7 : Small.{u, u_2} 𝒰.I₀] →
                            [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P] →
                              (i : 𝒰.I₀) →
                                (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).obj d.glued ≅
                                  (d.cocone i).pt
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The canonical linear map to the Hausdorffification.  -/
Hausdorffification.of : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M →ₗ[R] Hausdorffification I M
-- Mathlib.RingTheory.DividedPowers.Basic
dividedPowersBot_dpow_eq : ∀ {A : Type u_1} [inst : CommSemiring A] [inst_1 : DecidableEq A] (n : ℕ) (a : A),
  (dividedPowersBot A).dpow n a = if a = 0 ∧ n = 0 then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_two : ∀ (x : NNReal), x ^ 2 = x ^ 2
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.comm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} (self : E.Hom E') (r r' : ℤ)
  (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7) {Z : C} (h : (E'.page r' ⋯).X pq ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (self.hom r ⋯) pq)
      (CategoryTheory.CategoryStruct.comp (E'.iso r r' pq ⋯ ⋯).hom h) =
    CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom
      (CategoryTheory.CategoryStruct.comp ((self.hom r' ⋯).f pq) h)
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.ofTypeFunctor_obj : ∀ (m : Type u → Type v) [inst : Functor m] [inst_1 : LawfulFunctor m] (x : Type u),
  (CategoryTheory.ofTypeFunctor m).obj x = m x
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsComplProd_apply : ∀ {E : Type u_2} [inst : AddCommGroup E] {F : Type u_3} [inst_1 : AddCommGroup F] {R₁ : Type u_7} [inst_2 : CommRing R₁]
  [inst_3 : Module R₁ E] [inst_4 : Module R₁ F] {p q : Submodule R₁ E} (h : IsCompl p q)
  (φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)), (LinearMap.ofIsComplProd h) φ = LinearMap.ofIsCompl h φ.1 φ.2
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometryEquiv.toAffineIsometryEquiv_toAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (e : V ≃ₗᵢ[𝕜] V₂),
  e.toAffineIsometryEquiv.toAffineEquiv = e.toAffineEquiv
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_obj_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) {X_1 Y : D}
  (g : X_1 ⟶ Y),
  ((CategoryTheory.Functor.curry.obj F).obj X).map g =
    F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.interior_paramSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  interior (NumberField.mixedEmbedding.fundamentalCone.paramSet K) =
    Set.univ.pi fun w => if w = NumberField.Units.dirichletUnitTheorem.w₀ then Set.Iio 0 else Set.Ioo 0 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α},
  l.length ≤ (Std.Internal.List.insertListIfNewUnit l toInsert).length
-- Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Set.mem_prod_list_ofFn : ∀ {α : Type u_1} [inst : Monoid α] {n : ℕ} {a : α} {s : Fin n → Set α},
  a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_mk_eq_max : ∀ {α β : Type u} [Infinite α] [Infinite β], Cardinal.mk α * Cardinal.mk β = max (Cardinal.mk α) (Cardinal.mk β)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The projection from `StructuredArrow K B` to `C` creates any connected colimit.  -/
CategoryTheory.StructuredArrow.instCreatesColimitsOfShapeProjOfIsConnected : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            {K : CategoryTheory.Functor C D} →
              [CategoryTheory.IsConnected J] →
                {B : D} → CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.StructuredArrow.proj B K)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F), RingCat.Colimits.descFunLift F s RingCat.Colimits.Prequotient.zero = 0
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, with a set used for the pullback possibly larger.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [CompleteSpace E]
  [inst_12 : IsManifold I 1 M] [inst_13 : IsManifold I' 1 M'] {u : Set M},
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t y₀ →
    ContMDiffWithinAt I I' n f u x₀ →
      (mfderiv[u] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              f ⁻¹' t ∈ nhdsWithin x₀ s →
                s ⊆ u →
                  f x₀ = y₀ →
                    ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V u x⟩) s x₀
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- For any product along `{0, ..., n - 1}` of a commutative-monoid-valued function, we can verify
that it's equal to a different function just by checking ratios of adjacent terms up to `n`.

This is a multiplicative discrete analogue of the fundamental theorem of calculus.  -/
Finset.prod_range_induction : ∀ {M : Type u_4} [inst : CommMonoid M] (f s : ℕ → M),
  s 0 = 1 → ∀ (n : ℕ), (∀ k < n, s (k + 1) = s k * f k) → ∏ k ∈ Finset.range n, f k = s n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Roc α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Data.PSigma.Order
PSigma.Lex.denselyOrdered : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [DenselyOrdered ι] [∀ (i : ι), Nonempty (α i)]
  [inst_3 : (i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)], DenselyOrdered (Σₗ' (i : ι), α i)
-- Mathlib.Tactic.GCongr.Core
/-- The new goals produced by `gcongr`. This includes side-goals and main goals.
TODO?: split this into separate side and main goals, so that the side goals can be
discharged using a nested `gcongr by ...` syntax.  -/
Mathlib.Tactic.GCongr.State.newGoals : Mathlib.Tactic.GCongr.State → Array Lean.MVarId
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.uniformEquiv_toEquiv : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : UniformSpace X],
  Metric.Snowflaking.uniformEquiv.toEquiv = Metric.Snowflaking.ofSnowflaking
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.fixupSnippet : Lean.VersoModuleDocs.Snippet → Lean.Doc.DocM Lean.VersoModuleDocs.Snippet