mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.HomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono φ h).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h.left
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).f' = S.f
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofBitVec : ∀ {a : BitVec 32}, { toBitVec := a }.toNat = a.toNat
-- Init.Internal.Order.Basic
Lean.Order.Example.findF : (ℕ → Bool) → (ℕ → Option ℕ) → ℕ → Option ℕ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β},
  m.WF → (m.modify k f)[k']? = if (k == k') = true then Option.map f m[k]? else m[k']?
-- Mathlib.Data.NNReal.Defs
NNReal.instDenselyOrdered : DenselyOrdered NNReal
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, then for any `F`-linearly independent families
`{ u_i }`, `{ v_j }` of `A`, `B`, the products `{ u_i * v_j }`
are linearly independent over `F`.  -/
IntermediateField.LinearDisjoint.linearIndependent_mul : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A.LinearDisjoint ↥B →
    ∀ {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B},
      LinearIndependent F a → LinearIndependent F b → LinearIndependent F fun i => ↑(a i.1) * ↑(b i.2)
-- Mathlib.Tactic.AddGroup
/-- `add_group` normalizes expressions in additive groups without assuming commutativity. Unlike
`abel`, which does take advantage of commutativity, `add_group` instead only uses the additive
group axioms without any information about which group is manipulated. If the goal is an equality,
and after normalization the two sides are equal, `add_group` closes the goal.

`add_group at l1 l2 ...` normalizes at the given locations.

For additive commutative groups, use the `abel` tactic instead.
For multiplicative groups, use the `group` tactic instead.

Example:
```lean
example {G : Type} [AddGroup G] (a b c d : G) (h : c = (a + 2 • b) + (-(b + b) + (-a)) + d) :
    a + c + (-d) = a := by
  add_group at h -- normalizes `h` which becomes `h : c = d`
  rw [h]         -- the goal is now `a + d + (-d) = a`
  add_group      -- which is then normalized and closed
```
 -/
Mathlib.Tactic.AddGroup.addGroup : Lean.ParserDescr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.keysArray.toList = m.keys
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {k : ℕ}, IsPrimitiveRoot ζ k → ζ ^ k = 1
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.mk.sizeOf_spec : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : SizeOf k] [inst_3 : SizeOf G] (V : Type w)
  [hV1 : AddCommGroup V] [hV2 : Module k V] (ρ : Representation k G V),
  sizeOf { V := V, hV1 := hV1, hV2 := hV2, ρ := ρ } = 1 + sizeOf V + sizeOf hV1 + sizeOf hV2 + sizeOf ρ
-- Lean.Parser.Command
Lean.Parser.Command.protected : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Action.Limits
Action.forget₂_linear : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {R : Type u_3} [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R V]
  {FV : V → V → Type u_4} {CV : V → Type u_5} [inst_5 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_6 : CategoryTheory.ConcreteCategory V FV],
  CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (Action V G) V)
-- Mathlib.Data.Multiset.Filter
Multiset.filter_congr : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {s : Multiset α},
  (∀ x ∈ s, p x ↔ q x) → Multiset.filter p s = Multiset.filter q s
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.algebraMap_intTrace : ∀ {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [IsScalarTower A K L] [inst_10 : Algebra B L] [IsScalarTower A B L]
  [IsIntegralClosure B A L] [FiniteDimensional K L] [inst_14 : IsDomain A] [inst_15 : IsIntegrallyClosed A]
  [inst_16 : IsDomain B] [inst_17 : IsIntegrallyClosed B] [inst_18 : Module.Finite A B]
  [inst_19 : Module.IsTorsionFree A B] (x : B),
  (algebraMap A K) ((Algebra.intTrace A B) x) = (Algebra.trace K L) ((algebraMap B L) x)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_ne_zero_iff_nonempty : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r], Ordinal.type r ≠ 0 ↔ Nonempty α
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.isometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), Isometry ⇑f
-- Init.Data.Array.Range
Array.not_mem_range_self : ∀ {n : ℕ}, n ∉ Array.range n
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.nValue.eq_1 : ∀ (N : ℕ), Behrend.nValue N = ⌈√(Real.log ↑N)⌉₊
-- Lean.Environment
Lean.Kernel.Exception.declHasFVars.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (expr : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.declHasFVars env name expr) = 1 + sizeOf env + sizeOf name + sizeOf expr
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.leftInv_coeff_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E), p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Icc : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b r : K},
  0 < r → r • Set.Icc a b = Set.Icc (r * a) (r * b)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearMap_ofBijective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f),
  (AlgEquiv.ofBijective f hf).toLinearMap = ↑f
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.instInv : {K : Type u_1} → [Field K] → {a b : K} → Inv (QuadraticAlgebra K a b)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isLittleO_pow_exp_atTop : ∀ {n : ℕ}, (fun x => x ^ n) =o[Filter.atTop] Real.exp
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.splitter : {β : Type u_3} →
  {γ : Type u_1} →
    {init : γ} →
      (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
        (out : β) →
          (motive : Subtype (PlausibleForInStep out init) → Sort u_2) →
            (__do_lift : Subtype (PlausibleForInStep out init)) →
              ((c : γ) →
                  (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩) →
                ((c : γ) →
                    (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩) →
                  motive __do_lift
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.filter_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop),
  (π.filter p).boxes = {J ∈ π.boxes | p J}
-- Mathlib.Tactic.CongrExclamation
/-- A configuration option that makes `congr!` do the sorts of aggressive unfoldings that `congr`
does while also similarly preventing `congr!` from considering partial applications or congruences
between different functions being applied.  -/
Congr!.Config.unfoldSameFun : Congr!.Config
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcKeepAliveParams : Lean.FromJson Lean.Lsp.RpcKeepAliveParams
-- Mathlib.Order.Filter.Lift
Filter.comap_eq_lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, Filter.comap m f = f.lift' (Set.preimage m)
-- Mathlib.Order.Bounds.Image
/-- A monotone map sends a least element of a set to a least element of its image.  -/
Monotone.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {a : α} {s : Set α}, IsLeast s a → IsLeast (f '' s) (f a)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_apply_eq_bot_iff : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a : WithBot (σ →₀ ℕ)), m.toWithBotSyn a = ⊥ ↔ a = ⊥
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
/-- The cochain map `homogeneousCochains X ⟶ homogeneousCochains Y` induced by a continuous
group homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
`f : res φ X ⟶ Y`, sending an invariant function `σ : C(G, C(G, ⋯))` to `f ∘ σ ∘ φ`.  -/
ContinuousCohomology.cochainsMap : {k : Type u} →
  {G H : Type v} →
    [inst : Ring k] →
      [inst_1 : TopologicalSpace k] →
        [inst_2 : Group G] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              [inst_5 : Group H] →
                [inst_6 : TopologicalSpace H] →
                  [inst_7 : IsTopologicalGroup H] →
                    {X : TopRep k G} →
                      {Y : TopRep k H} →
                        (φ : H →ₜ* G) → (TopRep.res (↑φ) X ⟶ Y) → (X.homogeneousCochains ⟶ Y.homogeneousCochains)
-- Mathlib.GroupTheory.Descent
/-- If `G` is a commutative group and `n : ℕ`, `h : G → ℝ` satisfy
* `G / G ^ n` is finite,
* for all `g x : G`, `h x ≤ a * h (g * x) + c g`,
* for all `x : G`, `h (x ^ n) ≥ b * h x - c₀`,
* for all `B : ℝ`, there are only finitely many `x : G` such that `h x ≤ B`,

where `0 ≤ a < b` and `c₀` are real numbers, `c : G → ℝ`, then `G` is finitely generated.
 -/
CommGroup.fg_of_descent : ∀ {G : Type u_1} [inst : CommGroup G] {n : ℕ} {h : G → ℝ} {a b c₀ : ℝ} {c : G → ℝ},
  0 ≤ a →
    a < b →
      (powMonoidHom n).range.FiniteIndex →
        (∀ (g x : G), h x ≤ a * h (g * x) + c g) → (∀ (x : G), b * h x - c₀ ≤ h (x ^ n)) → ∀ [Northcott h], Group.FG G
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.exportDef.axdef : String → Lean.Name → Lean.Expr → List Lean.Name → Lean.ExportM Unit
-- Aesop.Rule
Aesop.SafeRule : Type
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.coeff_expand : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) {n : ℕ},
  (PowerSeries.coeff n) ((PowerSeries.expand p hp) φ) = if p ∣ n then (PowerSeries.coeff (n / p)) φ else 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_le_maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true
-- Init.Data.Fin.Bitwise
Fin.xor_val_of_uInt8Size : ∀ (a b : Fin UInt8.size), ↑(a ^^^ b) = ↑a ^^^ ↑b
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.haarProduct.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (K₀ : Set G),
  MeasureTheory.Measure.haar.haarProduct K₀ = Set.univ.pi fun K => Set.Icc 0 ↑(MeasureTheory.Measure.haar.index (↑K) K₀)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.right_nonuniformWitnesses_card : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t → ↑t.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).2.card
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.isRightAdjoint_pullback : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X Y : T}
  [P.IsStableUnderComposition] (f : X ⟶ Y) [inst_2 : P.HasPullbacksAlong f] [inst_3 : P.IsStableUnderBaseChangeAlong f],
  P f → (CategoryTheory.MorphismProperty.Over.pullback P ⊤ f).IsRightAdjoint
-- Init.Data.Nat.Gcd
Nat.gcd_le_left : ∀ {m : ℕ} (n : ℕ), 0 < m → m.gcd n ≤ m
-- Mathlib.Algebra.Notation.Lemmas
dite_lt_one : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LT α],
  (∀ (h : p), a h < 1) → (∀ (h : ¬p), b h < 1) → dite p a b < 1
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.GeneralLinearGroup.parabolicFixedPoint.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] (g : GL (Fin 2) K),
  g.parabolicFixedPoint = if ↑g 1 0 = 0 then OnePoint.infty else ↑((↑g 0 0 - ↑g 1 1) / (2 * ↑g 1 0))
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.lower_le_lower : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π → I.lower ≤ J.lower
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_add_left_mul : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x, y + x * z} = Ideal.span {x, y}
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.NatIso.prod_inv : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F F' : CategoryTheory.Functor A B} {G G' : CategoryTheory.Functor C D}
  (e₁ : F ≅ F') (e₂ : G ≅ G'), (CategoryTheory.NatIso.prod e₁ e₂).inv = CategoryTheory.NatTrans.prod e₁.inv e₂.inv
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
/-- An element `x` of a commutative local semiring is not contained in the maximal ideal
iff it is a unit.
 -/
IsLocalRing.notMem_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {x : R}, x ∉ IsLocalRing.maximalIdeal R ↔ IsUnit x
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.Presentation.naive.congr_simp : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s s_1 : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R) (e_s : s = s_1)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x),
  Algebra.Presentation.naive s hs = Algebra.Presentation.naive s_1 ⋯
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.PreDiscrTree.mk.inj : ∀ {α : Type} {root : Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ}
  {tries : Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α))}
  {root_1 : Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ}
  {tries_1 : Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α))},
  { root := root, tries := tries } = { root := root_1, tries := tries_1 } → root = root_1 ∧ tries = tries_1
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleAlgebra.mk : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieAdmissibleRing L] →
        [toModule : Module R L] →
          [toIsScalarTower : IsScalarTower R L L] → [toSMulCommClass : SMulCommClass R L L] → LieAdmissibleAlgebra R L
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.ExtDTreeMap.Const.maxEntry? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → Option (α × β)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mk.inj : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {toSlashInvariantForm : SlashInvariantForm Γ k}
  {holo' : MDiff ⇑toSlashInvariantForm}
  {bdd_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm.toFun k}
  {toSlashInvariantForm_1 : SlashInvariantForm Γ k} {holo'_1 : MDiff ⇑toSlashInvariantForm_1}
  {bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm_1.toFun k},
  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := bdd_at_cusps' } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := bdd_at_cusps'_1 } →
    toSlashInvariantForm = toSlashInvariantForm_1
-- Init.Data.Array.Find
Array.findIdx_eq_getD_findIdx? : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.findIdx p xs = (Array.findIdx? p xs).getD xs.size
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Ioc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo b a ⊆ Set.Ioc b a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, (I ⊓ J).ideal = I.ideal ⊓ J.ideal
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.terminalComparison F) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (F.obj A)) h
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_ofArray : ∀ {n : ℕ} (arr : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray arr).ReadyForRupAdd
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.ofField.congr_simp : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S S_1 : Submonoid A) (e_S : S = S_1) (hS : S ≤ nonZeroDivisors A)
  [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K],
  Localization.subalgebra.ofField K S hS = Localization.subalgebra.ofField K S_1 ⋯
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.instIsAccessibleComp : ∀ {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)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.IsAccessible.{w, v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Functor.IsAccessible.{w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Functor.IsAccessible.{w, v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addMap_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Equation Q →
      P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧
-- Mathlib.Topology.ContinuousMap.Basic
/-- The identity as a continuous map.  -/
ContinuousMap.id : (α : Type u_1) → [inst : TopologicalSpace α] → C(α, α)
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.instTopologicalSpace : {X : Type u_1} → [inst : TopologicalSpace X] → TopologicalSpace (T2Quotient X)
-- Mathlib.Algebra.Opposites
MulOpposite.unop_add : ∀ {α : Type u_1} [inst : Add α] (x y : αᵐᵒᵖ), MulOpposite.unop (x + y) = MulOpposite.unop x + MulOpposite.unop y
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instPartialOrderOpenAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenAddSubgroup G)
-- Mathlib.Data.Set.MemPartition
instFinite_memPartition : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ), Finite ↑(memPartition f n)
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
ContDiff.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {n : ℕ∞},
  ContDiff ℝ (↑n) c →
    ContDiff ℝ (↑n) R →
      ContDiff ℝ (↑n) x → (∀ (a : E), x a ≠ c a) → ContDiff ℝ ↑n fun a => EuclideanGeometry.inversion (c a) (R a) (x a)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] (p : Polynomial R) (t : R),
  Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (Polynomial.derivative p)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
Given a family of continuous linear maps `f : Π i, E i →L[𝕜] E₁ i`,
this function returns a continuous linear maps between the spaces of continuous multilinear maps
on `Π i, E₁ i` and on `Π i, E i`.
The map sends `g` to the map given by `v ↦ g (fun i ↦ f i (v i))`.

Actually, the map is multilinear in `f`,
see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.

For a version fixing `g` and varying `f`, see `compContinuousLinearMapLRight`.  -/
ContinuousMultilinearMap.compContinuousLinearMapL : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    {E : ι → Type u_3} →
      {F : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : (i : ι) → TopologicalSpace (E i)] →
            [inst_2 : (i : ι) → AddCommGroup (E i)] →
              [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        {E₁ : ι → Type u_5} →
                          [inst_8 : (i : ι) → TopologicalSpace (E₁ i)] →
                            [inst_9 : ContinuousConstSMul 𝕜 F] →
                              [inst_10 : (i : ι) → AddCommGroup (E₁ i)] →
                                [inst_11 : (i : ι) → Module 𝕜 (E₁ i)] →
                                  ((i : ι) → E i →L[𝕜] E₁ i) →
                                    ContinuousMultilinearMap 𝕜 E₁ F →L[𝕜] ContinuousMultilinearMap 𝕜 E F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.forIn_eq_forInUncurried : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.forIn f init t = Std.DTreeMap.Const.forInUncurried (fun a b => f a.1 a.2 b) init t
-- Init.Data.BitVec.Lemmas
BitVec.clz_eq_iff_eq_zero : ∀ {w : ℕ} {x : BitVec w}, x.clz = ↑w ↔ x = 0#w
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHoms_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} (φ : (p : ℤ) → F.X p ⟶ G.X p) (ψ : (p : ℤ) → G.X p ⟶ K.X p),
  (CochainComplex.HomComplex.Cochain.ofHoms φ).comp (CochainComplex.HomComplex.Cochain.ofHoms ψ) ⋯ =
    CochainComplex.HomComplex.Cochain.ofHoms fun p => CategoryTheory.CategoryStruct.comp (φ p) (ψ p)