mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_surjective_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H)
  [inst_2 : M.Normal] (f : G →* H),
  Function.Surjective (QuotientGroup.mk ∘ ⇑f) →
    ∀ (h : N ≤ Subgroup.comap f M), Function.Surjective ⇑(QuotientGroup.map N M f h)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of the pointwise negative of a tuple
equals its multiplicative height.  -/
Height.mulHeight_neg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K),
  Height.mulHeight (-x) = Height.mulHeight x
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_le_iff_le_comap : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂},
  Submodule.map f p ≤ q ↔ p ≤ Submodule.comap f q
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.c : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Weekday
-- Mathlib.AlgebraicGeometry.Scheme
/-- The zero locus of a set of sections `s` over an open set `U` is the closed set consisting of
the complement of `U` and of all points of `U`, where all elements of `f` vanish.
 -/
AlgebraicGeometry.Scheme.zeroLocus : (X : AlgebraicGeometry.Scheme) → {U : X.Opens} → Set ↑(X.presheaf.obj (Opposite.op U)) → Set ↥X
-- Mathlib.Order.Basic
PUnit.max_eq : ∀ (a b : PUnit.{u_5 + 1}), max a b = PUnit.unit
-- Std.Http.Data.URI.Basic
/-- Extracts all unique query parameter names.
 -/
Std.Http.URI.Query.names : Std.Http.URI.Query → Array Std.Http.URI.EncodedQueryParam
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k k' : α} {v : β},
      Array.find? (fun a => a.1 == k) (Std.DHashMap.Raw.Const.toArray ↑m) = some (k', v) ↔
        m.getKey? k = some k' ∧ Std.DHashMap.Internal.Raw₀.Const.get? m k = some v
-- Lean.Data.PersistentArray
Lean.PersistentArray.tooBig : ℕ
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
swap_integral : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F]
  (f : X → E × F), (∫ (x : X), f x ∂μ).swap = ∫ (x : X), (f x).swap ∂μ
-- Mathlib.Data.Sign.Basic
SignType.castHom_apply : ∀ {α : Type u_1} [inst : MulZeroOneClass α] [inst_1 : HasDistribNeg α] (a : SignType), SignType.castHom a = ↑a
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp_weightMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7}
  {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁]
  [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
  {P₂ : RootPairing ι₂ R M₂ N₂} (g : P₁.Hom P₂) (f : P.Hom P₁) (x : M),
  (g.comp f).weightMap x = g.weightMap (f.weightMap x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.inter_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)
-- Mathlib.Topology.Category.Profinite.CofilteredLimit
/-- Any locally constant function from a cofiltered limit of profinite sets factors through
one of the components.  -/
Profinite.exists_locallyConstant : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
  {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1}
  (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α),
  ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
/-- **Inclusion-exclusion principle** for the cardinality of an intersection of complements.

The cardinality of the intersection of the complements of the `S i` over `i ∈ s` is the
alternating sum of the cardinalities of the intersections of the `S i`.  -/
Finset.inclusion_exclusion_card_inf_compl : ∀ {ι : Type u_1} {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset ι) (S : ι → Finset α),
  ↑(s.inf fun i => (S i)ᶜ).card = ∑ t ∈ s.powerset, (-1) ^ t.card * ↑(t.inf S).card
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loop.wf.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc acc_1 : γ),
  acc = acc_1 →
    ∀ (next next_1 : α) (e_next : next = next_1) (h : LargeEnough next)
      (f f_1 : (out : α) → LargeEnough out → (c : γ) → n { s // Pl out c s }),
      f = f_1 →
        Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next h f =
          Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc_1 next_1 ⋯ f_1
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.X₃ = sq.X₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.continuous_starAlgHom : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S] [inst_10 : Ring A]
  [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S]
  [inst_18 : TopologicalSpace A] {a : A} {φ : C(↑(spectrum S a), S) →⋆ₐ[S] A},
  Continuous ⇑φ → ∀ {f : C(S, R)} (h : SpectrumRestricts a ⇑f), Continuous ⇑(SpectrumRestricts.starAlgHom φ h)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_map_equiv_to_embedding : ∀ {α : Type u_4} {β : Type u_5} [inst : Fintype α] [inst_1 : Fintype β] (e : α ≃ β),
  Finset.map e.toEmbedding Finset.univ = Finset.univ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.exists_length_eq_one_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, (∃ p, p.length = 1) ↔ G.Adj u v
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {w₀ : NumberField.InfinitePlace K},
  w₀.IsReal →
    ∀ {B : NNReal},
      NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B →
        ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < ↑(max B 1)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.mkResult : Lean.Meta.Grind.Params → Option Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Result
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit : Type
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.range_asIdeal : ∀ (R : Type u_1) [inst : CommSemiring R], Set.range MaximalSpectrum.asIdeal = {J | J.IsMaximal}
-- Mathlib.Algebra.Category.FGModuleCat.Basic
_private.Mathlib.Algebra.Category.FGModuleCat.Basic.0.FGModuleCat.evaluation_coevaluation : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (FGModuleCat.FGModuleCatCoevaluation K V) V)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator V (FGModuleCat.FGModuleCatDual K V) V).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (FGModuleCat.FGModuleCatEvaluation K V))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findSomeRev?TR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α), List.findSomeRev?TR f l = List.findSome? f l.reverse
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsNonloopAt.inc : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsNonloopAt e x → G.Inc e x
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_sum : ∀ (α : Type u_3) (β : Type u_4), ENat.card (α ⊕ β) = ENat.card α + ENat.card β
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1InfRes_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupCohomology.H1InfRes A S).g =
    groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) 1
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.funLike : (Γ : Subgroup (GL (Fin 2) ℝ)) → (k : ℤ) → FunLike (ModularForm Γ k) UpperHalfPlane ℂ
-- Init.Data.List.Basic
List.getLastD_nil : ∀ {α : Type u} {a : α}, [].getLastD a = a
-- Init.Data.BitVec.Lemmas
BitVec.toNat_eq : ∀ {n : ℕ} {x y : BitVec n}, x = y ↔ x.toNat = y.toNat
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
rootsOfUnityCircleEquiv.congr_simp : ∀ (n : ℕ) [inst : NeZero n], rootsOfUnityCircleEquiv n = rootsOfUnityCircleEquiv n
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_eq_true : ∀ {α : Type u} [inst : AddMonoidWithOne α] {a b : α} {c : ℕ},
  Mathlib.Meta.NormNum.IsNat a c → Mathlib.Meta.NormNum.IsNat b c → a = b
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.coe_quotientInfToSupQuotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  ⇑(LinearMap.quotientInfToSupQuotient p p') = ⇑(LinearMap.quotientInfEquivSupQuotient p p')
-- Mathlib.Algebra.GroupWithZero.Basic
zero_div : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), 0 / a = 0
-- Mathlib.Algebra.Category.FGModuleCat.Colimits
FGModuleCat.instHasColimitsOfShapeOfFinCategory : ∀ {k : Type u} [inst : Ring k] (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.HasColimitsOfShape J (FGModuleCat k)
-- Init.Data.SInt.Bitwise
Int32.neg_one_or : ∀ {a : Int32}, -1 ||| a = -1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.closure_prod_zero : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : Set M),
  AddSubmonoid.closure (s ×ˢ {0}) = (AddSubmonoid.closure s).prod ⊥
-- Aesop.Tracing
Aesop.TraceOption.ruleSet : Aesop.TraceOption
-- Mathlib.Analysis.Complex.CanonicalDecomposition
Complex.CanonicalDecomp.mk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  MeromorphicOn f (Metric.closedBall 0 R) →
    MeromorphicNFOn g (Metric.closedBall 0 R) →
      (∀ u ∈ Metric.ball 0 R, g u ≠ 0) →
        f =ᶠ[Filter.codiscreteWithin (Metric.closedBall 0 R)]
            (∏ᶠ (u : ℂ), Complex.canonicalFactor R u ^ (-(MeromorphicOn.divisor f (Metric.ball 0 R)) u)) • g →
          Complex.CanonicalDecomp f g R
-- Mathlib.Order.Interval.Lex
NonemptyInterval.toLex_lt_toLex : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] {x y : NonemptyInterval α},
  toLex x < toLex y ↔ y.toProd.1 < x.toProd.1 ∨ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 < y.toProd.2
-- Init.Prelude
/-- Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each
element must be traversed to find the next element.

`List α` is isomorphic to `Array α`, but they are useful for different things:
* `List α` is easier for reasoning, and `Array α` is modeled as a wrapper around `List α`.
* `List α` works well as a persistent data structure, when many copies of the tail are shared. When
  the value is not shared, `Array α` will have better performance because it can do destructive
  updates.
 -/
List : Type u → Type u
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.source_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, JoinedIn F x y → x ∈ F
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
CategoryTheory.Limits.IsColimit.eq_iff' : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4}
  [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_3 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget C)] {F : CategoryTheory.Functor J C}
  [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t)
  {i : J} (x y : CategoryTheory.ToType (F.obj i)),
  (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y ↔
    ∃ j f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y
-- Mathlib.Algebra.GroupWithZero.Action.Basic
MulAction.injective₀ : ∀ {G₀ : Type u_2} {α : Type u_8} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] {a : G₀},
  a ≠ 0 → Function.Injective fun x => a • x
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.erase : {α : Type u_1} → [inst : BEq α] → α → Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.instAlgebraInfiniteAdeleRing : (K : Type u_1) → [inst : Field K] → Algebra K (NumberField.InfiniteAdeleRing K)
-- Batteries.Data.List.Lemmas
List.countBefore_cons_succ : ∀ {α : Type u_1} {xs : List α} {x : α} {i : ℕ} {a : α} [inst : BEq α],
  List.countBefore x (a :: xs) (i + 1) = List.countBefore x xs i + if (a == x) = true then 1 else 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A category `HasFiniteBiproducts` if it has a biproduct for every finite family of objects in `C`
indexed by a finite type.  -/
CategoryTheory.Limits.HasFiniteBiproducts.out : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.Limits.HasFiniteBiproducts C] (n : ℕ), CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C
-- Mathlib.Data.List.Triplewise
List.Triplewise.below : {α : Type u_1} →
  {p : α → α → α → Prop} →
    {motive : (a : List α) → List.Triplewise p a → Prop} → {a : List α} → List.Triplewise p a → Prop
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.match_1.eq_1 : ∀ {α : Type u_2} (n : ℕ) (motive : (x : ℕ) → x ≤ n → α → Sort u_1) (h : 0 ≤ n) (a : α)
  (h_1 : (h : 0 ≤ n) → (a : α) → motive 0 h a) (h_2 : (m : ℕ) → (h : m.succ ≤ n) → (a : α) → motive m.succ h a),
  (match 0, h, a with
    | 0, h, a => h_1 h a
    | m.succ, h, a => h_2 m h a) =
    h_1 h a
-- Mathlib.Order.Filter.Basic
Filter.monotone_principal : ∀ {α : Type u}, Monotone Filter.principal
-- Mathlib.Tactic.FunProp.Mor
/-- argument of type `α`  -/
Mathlib.Meta.FunProp.Mor.Arg.expr : Mathlib.Meta.FunProp.Mor.Arg → Lean.Expr
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.mismatched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos},
  startPos < endPos →
    (∀ (pos : s.Pos), startPos ≤ pos → pos < endPos → ¬String.Slice.Pattern.Model.MatchesAt pat pos) →
      String.Slice.Pattern.Model.IsValidSearchFrom pat endPos l →
        String.Slice.Pattern.Model.IsValidSearchFrom pat startPos
          (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l)
-- Batteries.Data.List.Perm
List.Subperm.getElem_idxInj_eq_getElem : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys) {i : Fin xs.length},
  ys[↑(h.idxInj i)] = xs[↑i]
-- Mathlib.Data.Set.Lattice
Set.biUnion_self : ∀ {α : Type u_1} (s : Set α), ⋃ x ∈ s, s = s
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.inverseCoeff.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (a : kˣ)
  (A : WittVector p k), WittVector.inverseCoeff a A 0 = ↑a⁻¹
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instContinuousConstSMul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] {M : Type u_5} [inst_8 : Monoid M]
  [inst_9 : DistribMulAction M F] [inst_10 : SMulCommClass 𝕜 M F] [inst_11 : ContinuousConstSMul M F],
  ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)
-- Lean.Environment
Lean.instBEqAsyncBranch.beq : Lean.AsyncBranch → Lean.AsyncBranch → Bool
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenConj_ne_zero : Real.goldenConj ≠ 0
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_id : ∀ (α : Type u_2) [inst : NonAssocSemiring α] [inst_1 : Preorder α], ⇑(OrderRingHom.id α) = id
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts],
  (HomotopicalAlgebra.trivialFibrations C).IsStableUnderRetracts
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toLinearPreorderPackage : {α : Type u} → [self : Std.LinearOrderPackage α] → Std.LinearPreorderPackage α
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly) (d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation)
  (c : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p d c) = 1 + sizeOf p + sizeOf d + sizeOf c
-- Init.Data.String.TakeDrop
/-- Rewinds `pos` as long as `pat` matches.
 -/
String.Pos.revSkipWhile : {ρ : Type} → {s : String} → s.Pos → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → s.Pos
-- Mathlib.Order.Monotone.Basic
StrictAnti.minimal_of_maximal_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → ∀ {a : α}, (∀ (p : β), p ≤ f a) → ∀ (x : α), a ≤ x
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- The projection map `Cocycle K L n →+ CohomologyClass K L n`.  -/
CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n : ℤ) → CochainComplex.HomComplex.Cocycle K L n →+ CochainComplex.HomComplex.CohomologyClass K L n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1)))
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  x = Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
        h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) ≍
      h_2 size k v l