mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String}, (s.takeWhile pat).isEmpty = !s.startsWith pat
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_eq_fallback : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a : α} {fallback : β}, m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback
-- Lean.Meta.MethodSpecs
Lean.getMethodSpecTheorem : Lean.Name → String → Lean.MetaM (Option Lean.Name)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.withTacticInfoContext : {α : Type} → Lean.Syntax → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRight.eq_1 : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : MulOneClass M] [inst_1 : CommMonoid N₁]
  [inst_2 : CommMonoid N₂] (e : N₁ ≃* N₂),
  e.monoidHomCongrRight = { toEquiv := e.monoidHomCongrRightEquiv, map_mul' := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.compare_getKey?_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true
-- Init.Data.Bool
Bool.or_eq_right_iff_imp : ∀ {a b : Bool}, (a || b) = b ↔ a = true → b = true
-- Mathlib.SetTheory.Cardinal.Rat
Cardinal.mkRat : Cardinal.mk ℚ = Cardinal.aleph0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.isRightAdjoint_post : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {Y : D} {G : CategoryTheory.Functor D T} [G.IsRightAdjoint], (CategoryTheory.Over.post G).IsRightAdjoint
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isEventuallyConstantTo : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (i : ℤ) (q : ℕ),
  autoParam (i ≤ n₀ + ↑q) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isEventuallyConstantTo._auto_1✝ →
    ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor✝ f n₀).comp
          (HomologicalComplex.eval C (ComplexShape.up ℤ) i)).IsEventuallyConstantTo
      (Opposite.op q)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs.injEq : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (k : ℤ) (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (k_1 : ℤ),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs c₁ c₂ k =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs c₁_1 c₂_1 k_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1 ∧ k = k_1)
-- Mathlib.LinearAlgebra.Finsupp.Span
Submodule.image_smul_top_eq_range_lsum : ∀ {R : Type u_1} {M : Type u_2} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set σ) (f : σ → R), f '' s • ⊤ = ((Finsupp.lsum R) fun i => f ↑i • LinearMap.id).range
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.homeomorph_mk_coe_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (a : X ≃ Y)
  (b : Continuous a.toFun) (c : Continuous a.invFun),
  ⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c }.symm = ⇑a.symm
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (L : CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject.HoCat C) D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject.HoCat C))],
  (HomotopicalAlgebra.CofibrantObject.toHoCat.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.pentagon_hom_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          (CategoryTheory.CategoryStruct.id Z))
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            Z).hom)
-- Mathlib.Order.Bounds.Basic
/-- An alternative constructor for `SemilatticeSup` using `IsLUB`.  -/
SemilatticeSup.ofIsLUB : {α : Type u_1} → [inst : PartialOrder α] → (sup : α → α → α) → (∀ (a b : α), IsLUB {a, b} (sup a b)) → SemilatticeSup α
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `p ≤ 0` from a ring equality `p = 0`.  -/
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq : Lean.Meta.Grind.Arith.Linear.RingEqCnstr →
  Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.re_inner_starProjection_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E), 0 ≤ RCLike.re (inner 𝕜 (K.starProjection v) v)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isSubstLike : Lean.Expr → Bool
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The supremum of iterating a function on x arbitrary often is a fixed point  -/
OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (h : x ≤ f x),
  OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.fixedPoints.iterateChain (↑f) x h) ∈ Function.fixedPoints ⇑f
-- Mathlib.Condensed.AB
Condensed.instAB5CondensedMod : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.AB5 (CondensedMod R)
-- Init.Data.SInt.Lemmas
Int16.toInt_sub : ∀ (a b : Int16), (a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 16)
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.ResiduallyFinite G ↔ ∀ (g : G), g ≠ 0 → ∃ H, g ∉ H
-- Lean.Meta.Sorry
/-- Evaluates `fn` on each `sorry` in the declaration.
 -/
Lean.Declaration.forEachSorryM : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] → [MonadControlT Lean.MetaM m] → Lean.Declaration → (Lean.Expr → m Unit) → m Unit
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.castAdd m) (Finset.Ico i j) = Finset.Ico (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.exponentialPDF_eq : ∀ (r x : ℝ), ProbabilityTheory.exponentialPDF r x = ENNReal.ofReal (if 0 ≤ x then r * Real.exp (-(r * x)) else 0)
-- Mathlib.Computability.Partrec
Computable.list_append : ∀ {α : Type u_1} [inst : Primcodable α], Computable₂ fun x1 x2 => x1 ++ x2
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_lt_coe : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : Heyting.Regular α}, ↑a < ↑b ↔ a < b
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

O(1). Rebalance a tree which was previously balanced but has had its right
side grow by 1, or its left side shrink by 1.  -/
Ordnode.balanceR : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.quasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Abelian C] [inst_3 : (i : I) → CategoryTheory.Abelian (D i)]
      [inst_4 : CategoryTheory.CategoryWithHomology C]
      [inst_5 : ∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)]
      [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] {α : Type u_4} {c : ComplexShape α}
      {K L : HomologicalComplex C c} (f : K ⟶ L),
      QuasiIso f ↔ ∀ (i : I), QuasiIso (((F i).mapHomologicalComplex c).map f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Delaborates a finset indexing a big operator.  -/
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.delabFinsetResult : Lean.PrettyPrinter.Delaborator.DelabM BigOperators.FinsetResult✝
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Two closed sets are at zero Hausdorff edistance if and only if they coincide.  -/
IsClosed.hausdorffEDist_zero_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  IsClosed s → IsClosed t → (Metric.hausdorffEDist s t = 0 ↔ s = t)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : Option β → Option β) (l : List ((_ : α) × β)),
  Std.Internal.List.Const.alterKey k f l =
    match f (Std.Internal.List.getValue? k l) with
    | none => Std.Internal.List.eraseKey k l
    | some v => Std.Internal.List.insertEntry k v l
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.map'_eq_last_iff : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)),
  SimplexCategory.II.map' f x = Fin.last (n + 1) ↔ ∀ (i : Fin (n + 1)), (f i).castSucc < x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.OverMorphism.ext : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f g : U ⟶ V},
  CategoryTheory.Over.Hom.left f = CategoryTheory.Over.Hom.left g → f = g
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Move elements from `k₁` to `k₂` while `p` holds, with the last element being left on `k₁`.  -/
Turing.PartrecToTM2.moveExcl : (Turing.PartrecToTM2.Γ' → Bool) →
  Turing.PartrecToTM2.K' → Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.dist_lt_iff_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)} {C : ℝ} [Nonempty α], dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
-- Mathlib.Geometry.Manifold.Immersion
/-- `f : M → N` is a `C^n` immersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `u ↦ (u, 0)`.
Additionally, we demand that `f` map `φ.source` into `ψ.source`.

NB. We don't know the particular atlases used for `M` and `N`, so asking for `φ` and `ψ` to be
in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.

Implicit in this definition is an abstract choice `F` of a complement of `E` in `E'`: being an
immersion at `x` includes a choice of linear isomorphism between `E × F` and `E'`, which is
where the choice of `F` enters.
If you need stronger control over the complement `F`, use `IsImmersionAtOfComplement` instead.
 -/
Manifold.IsImmersionAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E'' G →
                            {M : Type u_11} →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst : TopologicalSpace N] → [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → M → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termZ₁ : Lean.ParserDescr
-- Mathlib.Algebra.CharP.Algebra
/-- A nontrivial `ℚ`-algebra has `CharP` equal to zero.

This cannot be a (local) instance because it would immediately form a loop with the
instance `DivisionRing.toRatAlgebra`. It's probably easier to go the other way: prove `CharZero R`
and automatically receive an `Algebra ℚ R` instance.
 -/
algebraRat.charP_zero : ∀ (R : Type u_3) [Nontrivial R] [inst : Semiring R] [Algebra ℚ R], CharP R 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Triangle inequality for the nonnegative distance  -/
nndist_triangle : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), nndist x z ≤ nndist x y + nndist y z
-- Mathlib.Order.JordanHolder
CompositionSeries.le_last_of_mem : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x : X},
  x ∈ s → x ≤ RelSeries.last s
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractiveAux.withIgnoreTags : Std.Format → Lean.Widget.MsgFmtM✝ Std.Format
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ico_eq_restrict_Icc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, μ.restrict (Set.Ico a b) = μ.restrict (Set.Icc a b)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.zero_eq_one_iff : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R}, 0 = 1 ↔ I = ⊤
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- The morphism part  -/
CategoryTheory.ProfunctorCore.map : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (self : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) →
          {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (self.obj X Y' ⟶ self.obj X' Y)
-- Mathlib.Tactic.Peel
/-- Given a list `l` of names, this peels `num` quantifiers off of the expression `e` and
the main goal and introduces variables with the provided names until the list of names is exhausted.
Note: the name `n?` (with default `this`) is used for the name of the expression `e` with
quantifiers peeled.  -/
Mathlib.Tactic.Peel.peelArgs : Lean.Expr → ℕ → List Lean.Name → Option Lean.Name → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonList : {α : Type u_1} → [Lean.FromJson α] → Lean.FromJson (List α)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `sub_apply`. -/
QuadraticMap.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsSupported.mk : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} {e : c.Embedding c'},
  (∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → K.ExactAt i') → K.IsSupported e
-- Mathlib.Algebra.Homology.Monoidal
/-- The unit of the tensor product of homological complexes.  -/
HomologicalComplex.tensorUnit : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [CategoryTheory.Limits.HasZeroObject C] →
          {I : Type u_2} → [AddMonoid I] → (c : ComplexShape I) → [DecidableEq I] → HomologicalComplex C c
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.ofSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [inst_2 : H.FiniteIndex],
  FiniteIndexNormalSubgroup.ofSubgroup H = { toSubgroup := H, isNormal' := ⋯, isFiniteIndex' := ⋯ }
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_eq_of_sub_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v (y - x) < v x → v y = v x
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.notFollowedBy.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If two groups `H` and `G` act on a topological space `X` such that `G` acts properly and
there exists a group homomorphism `H → G` which is a closed embedding compatible with the actions,
then `H` also acts properly on `X`.  -/
properSMul_of_isClosedEmbedding : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] {H : Type u_3} [inst_4 : Group H] [inst_5 : MulAction H X] [inst_6 : TopologicalSpace H]
  [ProperSMul G X] (f : H →* G), Topology.IsClosedEmbedding ⇑f → (∀ (h : H) (x : X), f h • x = h • x) → ProperSMul H X
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (y : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : L.HasTotal (ComplexShape.up ℤ)]
  {Z : HomologicalComplex C (ComplexShape.up ℤ)}
  (h :
    (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (L.total (ComplexShape.up ℤ)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₂ C y).map f) (ComplexShape.up ℤ))
      (CategoryTheory.CategoryStruct.comp (L.totalShift₂Iso y).hom h) =
    CategoryTheory.CategoryStruct.comp (K.totalShift₂Iso y).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map
          (HomologicalComplex₂.total.map f (ComplexShape.up ℤ)))
        h)
-- Init.Data.Vector.Lemmas
Vector.cast_rfl : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, Vector.cast ⋯ xs = xs
-- Mathlib.Data.Finsupp.AList
Finsupp.toAList_entries : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M), f.toAList.entries = List.map Prod.toSigma f.graph.toList
-- Mathlib.Data.ENNReal.Inv
ENNReal.toNNReal_inv : ∀ (a : ENNReal), a⁻¹.toNNReal = a.toNNReal⁻¹
-- Init.Data.Array.Lemmas
Array.uset.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : USize) (e_i : i = i_1) (v v_1 : α),
  v = v_1 → ∀ (h : i.toNat < xs.size), xs.uset i v h = xs_1.uset i_1 v_1 ⋯
-- Init.Data.Order.MinMaxOn
min_apply : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : Min β]
  [Std.LawfulOrderLeftLeaningMin β] {f : α → β} {x y : α}, f x ⊓ f y = f (minOn f x y)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- Any clifford algebra is isomorphic to the even subalgebra of a clifford algebra with an extra
dimension (that is, with vector space `M × R`), with a quadratic form evaluating to `-1` on that new
basis vector.  -/
CliffordAlgebra.equivEven : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → CliffordAlgebra Q ≃ₐ[R] ↥(CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q))
-- Mathlib.MeasureTheory.Function.EssSup
essSup_map_measure_of_measurable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β}
  [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace β] [SecondCountableTopology β] [OrderClosedTopology β]
  [OpensMeasurableSpace β],
  Measurable g →
    AEMeasurable f μ →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
          essSup_map_measure_of_measurable._auto_1 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
            essSup_map_measure_of_measurable._auto_3 →
          autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
              essSup_map_measure_of_measurable._auto_5 →
            autoParam
                (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
                essSup_map_measure_of_measurable._auto_7 →
              essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
-- Init.Data.Vector.Lemmas
Vector.map_inj : ∀ {n : ℕ} {α : Type u_1} {α_1 : Type u_2} {f g : α → α_1} [NeZero n], Vector.map f = Vector.map g ↔ f = g
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3)
  (node : Lean.PersistentHashMap.Node α β) (h_1 : Unit → motive Lean.PersistentHashMap.Entry.null)
  (h_2 : (k : α) → (v : β) → motive (Lean.PersistentHashMap.Entry.entry k v))
  (h_3 : (node : Lean.PersistentHashMap.Node α β) → motive (Lean.PersistentHashMap.Entry.ref node)),
  (match Lean.PersistentHashMap.Entry.ref node with
    | Lean.PersistentHashMap.Entry.null => h_1 ()
    | Lean.PersistentHashMap.Entry.entry k v => h_2 k v
    | Lean.PersistentHashMap.Entry.ref node => h_3 node) =
    h_3 node
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.scoped : {α : Type} → Lean.Name → α → Lean.ScopedEnvExtension.Entry α
-- Init.Data.Vector.Lemmas
Vector.mem_flatMap : ∀ {α : Type u_1} {β : Type u_2} {m n : ℕ} {f : α → Vector β m} {b : β} {xs : Vector α n},
  b ∈ xs.flatMap f ↔ ∃ a ∈ xs, b ∈ f a
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
/-- Let `u : E → F` be a continuous linear map, and `A` a closed subspace of `E` of finite
codimension. Then `u` is strict with closed range if and only if its restriction
`u.domRestrict A : A → F` is strict with closed range.

This is [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1, Prop. 1][bourbaki2023].  -/
ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E),
  IsClosed ↑A →
    ∀ [A.CoFG],
      Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔
        Topology.IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed ↑(↑(u.domRestrict A)).range
-- Lean.Data.Options
Lean.Option.get : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Option α → α