mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.RuleTac.Forward.Basic
/-- Mark hypotheses that, according to their name, are forward implementation detail
hypotheses, as implementation details. This is a hack that works around the
fact that certain tactics (particularly anything based on the revert-intro
pattern) can turn implementation detail hyps into regular hyps.
 -/
Aesop.hideForwardImplDetailHyps : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Homology.Homotopy
dNext_nat : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (C D : ChainComplex V ℕ) (i : ℕ) (f : (i j : ℕ) → C.X i ⟶ D.X j),
  (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i (i - 1)) (f (i - 1) i)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂'_comp : ∀ {n : Type u_11} {m : Type u_12} {n' : Type u_13} {R : Type u_16} [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype n'] [inst_6 : DecidableEq n']
  (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (n' → R) →ₗ[R] n → R),
  (LinearMap.toMatrix₂' R) (B ∘ₗ f) = (LinearMap.toMatrix' f).transpose * (LinearMap.toMatrix₂' R) B
-- Init.Data.List.Attach
List.pmap.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (a : α) (l : List α) (H : ∀ a_1 ∈ a :: l, P a_1),
  List.pmap f (a :: l) H = f a ⋯ :: List.pmap f l ⋯
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.to_image_id : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l.HasBasis (fun x => x ∈ s '' {i | p i}) id
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- The fundamental group of a path connected space is independent of the choice of basepoint.  -/
FundamentalGroup.fundamentalGroupMulEquivOfPathConnected : {X : Type u_1} →
  [inst : TopologicalSpace X] → (x₀ x₁ : X) → [PathConnectedSpace X] → FundamentalGroup X x₀ ≃* FundamentalGroup X x₁
-- Init.Data.Vector.Lemmas
Vector.getElem?_setIfInBounds_ne : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α}, i ≠ j → (xs.setIfInBounds i x)[j]? = xs[j]?
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n * log n). Build a set from a list, preferring elements that appear earlier in the list
in the case of equivalent elements.

```
ofList [1, 2, 3] = {1, 2, 3}
ofList [2, 1, 1, 3] = {1, 2, 3}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
ofList [(1, 1), (0, 1), (1, 2)] = {(0, 1), (1, 1)}
```  -/
Ordnode.ofList : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → List α → Ordnode α
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.epi_fst_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi g]
  {s : CategoryTheory.Limits.PullbackCone f g} (hs : CategoryTheory.Limits.IsLimit s), CategoryTheory.Epi s.fst
-- Mathlib.Topology.Algebra.MulAction
/-- A group action of a topological group on a discrete space is continuous if and only if
each stabilizer is an open subgroup.  -/
continuousSMul_iff_stabilizer_isOpen : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Group M]
  [IsTopologicalGroup M] [inst_4 : MulAction M X] [DiscreteTopology X],
  ContinuousSMul M X ↔ ∀ (x : X), IsOpen ↑(MulAction.stabilizer M x)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.piEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι' : Type u_7} {N : ι' → Type u_8} [inst_4 : (i : ι') → AddCommMonoid (N i)]
  [inst_5 : (i : ι') → TopologicalSpace (N i)] [inst_6 : (i : ι') → Module R (N i)] (f : M [⋀^ι]→L[R] ((i : ι') → N i))
  (i : ι'), ContinuousAlternatingMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousAlternatingMap f
-- Mathlib.LinearAlgebra.Pi
/-- The empty bilinear map defeq to `Matrix.vecEmpty`  -/
LinearMap.vecEmpty₂ : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        [inst : CommSemiring 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₃] → M →ₗ[R] M₂ →ₗ[R] Fin 0 → M₃
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_map_of_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Continuous (CompactCoherentification.map f)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.one_mul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : NonAssocSemiring B] [inst_6 : Module R B]
  [inst_7 : SMulCommClass R B B] [inst_8 : IsScalarTower R B B] (x : TensorProduct R A B),
  (Algebra.TensorProduct.mul (1 ⊗ₜ[R] 1)) x = x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {X : C} {addGrp : CategoryTheory.AddGrpObj X} {X_1 : C} {addGrp_1 : CategoryTheory.AddGrpObj X_1},
  { X := X, addGrp := addGrp } = { X := X_1, addGrp := addGrp_1 } → X = X_1 ∧ addGrp ≍ addGrp_1
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The exterior power of an object in `ModuleCat R`.  -/
ModuleCat.exteriorPower : {R : Type u} → [inst : CommRing R] → ModuleCat R → ℕ → ModuleCat R
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.isOrtho_inr_inr_iff : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} (m₂ m₂' : M₂),
  (Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.comp_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N K : CategoryTheory.Mat_ C} (f : M ⟶ N) (g : N ⟶ K),
  CategoryTheory.CategoryStruct.comp f g = fun i k => ∑ j, CategoryTheory.CategoryStruct.comp (f i j) (g j k)
-- Mathlib.Order.RelClasses
/-- A class for a well-founded relation `<`.  -/
WellFoundedLT : (α : Type u_1) → [LT α] → Prop
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_genEigenspace_top : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, x ∈ (f.genEigenspace μ) ⊤ ↔ ∃ k, x ∈ ((f - μ • 1) ^ k).ker
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → t.max! = t_1.max!
-- Mathlib.Order.Hom.Basic
OrderIso.monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), Monotone ⇑e
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.atLeastAux : ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.boolKernel_false : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  (ProbabilityTheory.Kernel.boolKernel μ ν) false = μ
-- Lean.DocString.Parser
Lean.Doc.Parser.instInhabitedBlockCtxt.default : Lean.Doc.Parser.BlockCtxt
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.roots_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R], f.Splits → f.natDegree ≠ 0 → f.roots ≠ 0
-- Mathlib.Topology.Algebra.ConstMulAction
continuousWithinAt_const_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G]
  [inst_2 : AddAction G α] [ContinuousConstVAdd G α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β}
  (c : G), ContinuousWithinAt (fun x => c +ᵥ f x) s b ↔ ContinuousWithinAt f s b
-- Mathlib.AlgebraicTopology.DoldKan.Notations
/-- The normalized Moore complex functor, on objects.
 -/
DoldKan.«termN[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Semiconj.Units
/-- If a unit `a` semiconjugates `x` to `y`, then `a⁻¹` semiconjugates `y` to `x`.  -/
SemiconjBy.units_inv_symm_left : ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} {x y : M}, SemiconjBy (↑a) x y → SemiconjBy (↑a⁻¹) y x
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.zipWithAll.go : {α : Type u} → {β : Type u_1} → {γ : Type u_2} → (Option α → Option β → γ) → Array α → Array β → ℕ → Array γ → Array γ
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_iInf : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, a - ⨅ i, f i = ⨆ i, a - f i
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_mul_apply_eq : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R) (i : n), (Matrix.adjp s A * A) i i = Matrix.detp s A
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientKerAlgEquivOfSurjective_apply : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f)
  (a : A ⧸ RingHom.ker f.toRingHom), (Ideal.quotientKerAlgEquivOfSurjective hf) a = (↑f).kerLift a
-- Init.Data.Ord.SInt
Int32.instOrd : Ord Int32
-- Std.Data.ExtHashMap.Basic
/-- Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.ExtHashMap.containsThenInsert : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → β → Bool × Std.ExtHashMap α β
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<$>`, weakest precondition version.
(Use this for reasoning backward from the goal.)
 -/
SatisfiesM.map_pre : ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p : α_1 → Prop} {f : α → α_1} [inst : Functor m] [LawfulFunctor m]
  {x : m α}, SatisfiesM (fun a => p (f a)) x → SatisfiesM p (f <$> x)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkNatIso_hom : ∀ {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 G : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (eₗ : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G)
  (eᵣ : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G))
      CategoryTheory.Join.mkNatIso._auto_1),
  (CategoryTheory.Join.mkNatIso eₗ eᵣ h).hom = CategoryTheory.Join.mkNatTrans eₗ.hom eᵣ.hom h
-- Mathlib.RingTheory.Localization.BaseChange
/-- The isomorphism `S ⊗[R] Rₘ ≃ₐ[S] Sₘ`. This is a specialization of `IsLocalization.algEquiv`,
but with additional properties since now `Sₘ` is automatically an `Rₘ`-algebra.  -/
Localization.tensorLeftAlgEquiv : {R : Type u_10} →
  [inst : CommRing R] →
    (M : Submonoid R) →
      (S : Type u_12) →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            TensorProduct R S (Localization M) ≃ₐ[S] Localization (Algebra.algebraMapSubmonoid S M)
-- Mathlib.Order.IsNormal
OrderIso.isNormal : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : α ≃o β), Order.IsNormal ⇑f
-- Init.Data.List.Nat.TakeDrop
List.getLast?_take : ∀ {α : Type u_1} {i : ℕ} {l : List α}, (List.take i l).getLast? = if i = 0 then none else l[i - 1]?.or l.getLast?
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.iSupIndep_genWeightSpaceOf : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [Module.IsTorsionFree R M] (x : L),
  iSupIndep fun χ => LieModule.genWeightSpaceOf M χ x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool}, Std.ExtDTreeMap.filter (fun k x => f k) t = t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = true
-- Mathlib.Logic.Encodable.Lattice
Encodable.iUnion_decode₂_cases : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable β] {f : β → Set α} {C : Set α → Prop},
  C ∅ → (∀ (b : β), C (f b)) → ∀ {n : ℕ}, C (⋃ b ∈ Encodable.decode₂ β n, f b)
-- Mathlib.Algebra.Order.Ring.GeomSum
Nat.geom_sum_le : ∀ {b : ℕ}, 2 ≤ b → ∀ (a n : ℕ), ∑ i ∈ Finset.range n, a / b ^ i ≤ a * b / (b - 1)
-- Mathlib.Data.ENNReal.Basic
ENNReal.instInhabited : Inhabited ENNReal
-- Mathlib.Computability.StateTransition
StateTransition.tr_eval_dom : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop},
  StateTransition.Respects f₁ f₂ tr →
    ∀ {a₁ : σ₁} {a₂ : σ₂}, tr a₁ a₂ → ((StateTransition.eval f₂ a₂).Dom ↔ (StateTransition.eval f₁ a₁).Dom)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.equation_iff_nonsingular : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W]
  {x y : R}, W.Equation x y ↔ W.Nonsingular x y
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_snd_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α}
  {b : β},
  (Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).2 =
    ↑(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).2
-- Mathlib.Data.Matrix.Composition
/-- `Matrix.comp` as `AddEquiv`  -/
Matrix.compAddEquiv : (I : Type u_1) →
  (J : Type u_2) →
    (K : Type u_3) →
      (L : Type u_4) → (R : Type u_5) → [inst : Add R] → Matrix I J (Matrix K L R) ≃+ Matrix (I × K) (J × L) R
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.ext : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} {f g : X.Path m}, f.vertex = g.vertex → f.arrow = g.arrow → f = g
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.mk.sizeOf_spec : ∀ (type proof : Lean.Expr) (argKinds : Array Lean.Meta.CongrArgKind),
  sizeOf { type := type, proof := proof, argKinds := argKinds } = 1 + sizeOf type + sizeOf proof + sizeOf argKinds
-- Mathlib.Topology.MetricSpace.PiNat
/-- The map from `X` to the subset of `∀ i, Y i`.  -/
Metric.PiNatEmbed.toPiNat : {ι : Type u_2} → {X : Type u_5} → {Y : ι → Type u_6} → {f : (i : ι) → X → Y i} → X → Metric.PiNatEmbed X Y f
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.instReprWeekday.repr.match_1.eq_7 : ∀ (motive : Std.Time.Weekday → Sort u_1) (h_1 : Unit → motive Std.Time.Weekday.monday)
  (h_2 : Unit → motive Std.Time.Weekday.tuesday) (h_3 : Unit → motive Std.Time.Weekday.wednesday)
  (h_4 : Unit → motive Std.Time.Weekday.thursday) (h_5 : Unit → motive Std.Time.Weekday.friday)
  (h_6 : Unit → motive Std.Time.Weekday.saturday) (h_7 : Unit → motive Std.Time.Weekday.sunday),
  (match Std.Time.Weekday.sunday with
    | Std.Time.Weekday.monday => h_1 ()
    | Std.Time.Weekday.tuesday => h_2 ()
    | Std.Time.Weekday.wednesday => h_3 ()
    | Std.Time.Weekday.thursday => h_4 ()
    | Std.Time.Weekday.friday => h_5 ()
    | Std.Time.Weekday.saturday => h_6 ()
    | Std.Time.Weekday.sunday => h_7 ()) =
    h_7 ()
-- Mathlib.Algebra.BigOperators.Pi
/-- The canonical isomorphism between the monoid of homomorphisms from a finite product of
commutative monoids to another commutative monoid and the product of the homomorphism monoids.  -/
Pi.monoidHomMulEquiv : {ι : Type u_7} →
  [Fintype ι] →
    [DecidableEq ι] →
      (M : ι → Type u_8) →
        [inst : (i : ι) → CommMonoid (M i)] →
          (M' : Type u_9) → [inst_1 : CommMonoid M'] → (((i : ι) → M i) →* M') ≃* ((i : ι) → M i →* M')
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- `exp ∘ f` is analytic  -/
AnalyticAt.cexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  AnalyticAt ℂ f x → AnalyticAt ℂ (Complex.exp ∘ f) x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.erase.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.erase a = m_1.erase a_1
-- Mathlib.Order.Hom.Lattice
LatticeHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β), f.toFun = ⇑f
-- Mathlib.Data.Seq.Computation
Computation.lift_eq_iff_equiv : ∀ {α : Type u} (c₁ c₂ : Computation α), Computation.LiftRel (fun x1 x2 => x1 = x2) c₁ c₂ ↔ c₁.Equiv c₂
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.toListRev_takeWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.takeWhile P it).toListRev = (List.takeWhile P it.toList).reverse
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.self_comp_symm_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.toHom.comp f.symm.toHom = FirstOrder.Language.Hom.id L N
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.mk.injEq : ∀ (foundLine foundFlattenedHardLine : Bool) (space : ℕ) (foundLine_1 foundFlattenedHardLine_1 : Bool) (space_1 : ℕ),
  ({ foundLine := foundLine, foundFlattenedHardLine := foundFlattenedHardLine, space := space } =
      { foundLine := foundLine_1, foundFlattenedHardLine := foundFlattenedHardLine_1, space := space_1 }) =
    (foundLine = foundLine_1 ∧ foundFlattenedHardLine = foundFlattenedHardLine_1 ∧ space = space_1)
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.mk.congr_simp : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (toLinearEquiv toLinearEquiv_1 : M₁ ≃ₗ[R] M₂)
  (e_toLinearEquiv : toLinearEquiv = toLinearEquiv_1)
  (map_app' : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv).toFun n)) ((↑toLinearEquiv).toFun m) = (B₁ n) m),
  { toLinearEquiv := toLinearEquiv, map_app' := map_app' } = { toLinearEquiv := toLinearEquiv_1, map_app' := ⋯ }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toArray_toList : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Mathlib.Topology.Path
/-- The constant path from a point to itself  -/
Path.refl : {X : Type u_1} → [inst : TopologicalSpace X] → (x : X) → Path x x
-- Mathlib.Analysis.Normed.Ring.Lemmas
SeparationQuotient.instNonUnitalNormedCommRing : {α : Type u_1} → [inst : NonUnitalSeminormedCommRing α] → NonUnitalNormedCommRing (SeparationQuotient α)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
/-- The canonical map from `K` to the finite adeles of `K`.

The content of the existence of this map is the fact that an element `k` of `K` is integral at
all but finitely many places, which is `IsDedekindDomain.HeightOneSpectrum.Support.finite R k`.
 -/
IsDedekindDomain.FiniteAdeleRing.algebraMap : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → K →+* IsDedekindDomain.FiniteAdeleRing R K
-- Mathlib.Data.Seq.Computation
/-- `destruct c` is the destructor for `Computation α` as a coinductive type.
It returns `inl a` if `c = pure a` and `inr c'` if `c = think c'`.  -/
Computation.destruct : {α : Type u} → Computation α → α ⊕ Computation α
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
/-- If `X ⟶ Spec ℤ` has affine diagonal (in particular when `X` is separated), then intersections
of affine opens of `X` are also affine.  -/
AlgebraicGeometry.IsAffineOpen.inf : ∀ {X : AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))]
  {U V : X.Opens},
  AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen V → AlgebraicGeometry.IsAffineOpen (U ⊓ V)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.mk.inj : ∀ {A : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} {left : X.left ⟶ Y.left} {right : X.right ⟶ Y.right}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map right))
      CategoryTheory.CommaMorphism.w._autoParam}
  {left_1 : X.left ⟶ Y.left} {right_1 : X.right ⟶ Y.right}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left_1) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R.map right_1))
      CategoryTheory.CommaMorphism.w._autoParam},
  { left := left, right := right, w := w } = { left := left_1, right := right_1, w := w_1 } →
    left = left_1 ∧ right = right_1
-- Lean.Elab.App
/-- Returns `fType` with loose bvars instantiated and metavariables instantiated.
Caches the result.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getFType' : Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.completeSpace_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (p : Submodule R E) [CompleteSpace ↥p], CompleteSpace ↥(Submodule.map (↑↑↑e) p)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.Intermediate.appendSnd.eq_1 : ∀ {m : Type w → Type w'} {β α₂ : Type w} [inst : Std.Iterator α₂ m β] (α₁ : Type w) (it₂ : Std.IterM m β),
  Std.IterM.Intermediate.appendSnd α₁ it₂ = { internalState := Std.Iterators.Types.Append.snd it₂ }
-- Init.Data.String.Modify
/-- Replaces the character at position `p` in the string `s` with the result of applying `f` to that
character. If `p` is an invalid position, the string is returned unchanged.

If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.

This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
`String.pos` or another means of obtaining a `String.Pos`.

Examples:
* `"abc".modify ⟨1⟩ Char.toUpper = "aBc"`
* `"abc".modify ⟨3⟩ Char.toUpper = "abc"`
 -/
String.Pos.Raw.modify : String → String.Pos.Raw → (Char → Char) → String