mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.Covering
/-- The path star at a vertex `u` is the type of all paths starting at `u`.
The type `Quiver.PathStar u` is defined to be `Σ v : U, Path u v`.  -/
Quiver.PathStar : {U : Type u_1} → [Quiver U] → U → Type (max u_1 u_1 u)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_list_const_inv : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
  {inv : β → Pred} {epost : EPred},
  (∀ (hd : α) (b : β),
      ⦃ inv b ⦄ f hd b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv b'
        | ForInStep.done b' => inv b';
        epost ⦄) →
    ⦃ inv init ⦄ forIn xs init f ⦃ inv; epost ⦄
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, a ∉ t → t.getKey! a = default
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_eq_subst_cert.eq_1 : ∀ (x : Lean.Grind.Linarith.Var) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_eq_subst_cert x p₁ p₂ p₃ = (p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initial.strict_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {A : C} (f g : A ⟶ ⊥_ C), f = g
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.egirth_top : ∀ {α : Type u_1}, 3 ≤ ENat.card α → ⊤.egirth = 3
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_smul_congr' : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : MeasurableSpace A] [inst_4 : TopologicalSpace A] [inst_5 : BorelSpace A] [inst_6 : IsTopologicalAddGroup A]
  [LocallyCompactSpace A] [inst_8 : ContinuousConstSMul G A] (μ : MeasureTheory.Measure A) {ν : MeasureTheory.Measure A}
  [inst_9 : μ.IsAddHaarMeasure] [inst_10 : ν.IsAddHaarMeasure] (g : Gᵈᵐᵃ),
  (g • μ).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
-- Mathlib.Data.Set.Image
Function.LeftInverse.preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → ∀ (s : Set α), f ⁻¹' g ⁻¹' s = s
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_mul_rev : ∀ {R : Type u} [inst : CommRing R] (f g : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hu₁ : U ≤ PrimeSpectrum.basicOpen g) (hu₂ : U ≤ PrimeSpectrum.basicOpen f),
  AlgebraicGeometry.StructureSheaf.const f g U hu₁ * AlgebraicGeometry.StructureSheaf.const g f U hu₂ = 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.refl_trans : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), (AffineEquiv.refl k P₁).trans e = e
-- Mathlib.RingTheory.Ideal.Basic
Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R], ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤
-- Std.Internal.Parsec.Basic
/-- Succeeds only if input is at end-of-file.
 -/
Std.Internal.Parsec.eof : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι Unit
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of coplanar points is finite-dimensional.  -/
Coplanar.finiteDimensional_vectorSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, Coplanar k s → FiniteDimensional k ↥(vectorSpan k s)
-- Init.Data.Sum.Lemmas
Sum.swap_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), x.swap.swap = x
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.noncommPiCoprod_range : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → AddGroup (H i)]
  (ϕ : (i : ι) → H i →+ G) [inst_2 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)},
  (AddMonoidHom.noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range
-- Mathlib.Logic.Basic
not_imp_self : ∀ {a : Prop}, ¬a → a ↔ a
-- Mathlib.Order.Nucleus
Nucleus.instInfSet : {X : Type u_1} → [inst : CompleteLattice X] → InfSet (Nucleus X)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_apply_tmul : ∀ {R : Type u_1} (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (M : Type u_4) [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : IsScalarTower R A M] {N : Type u_5} [inst_9 : AddCommGroup N] [inst_10 : Module R N]
  [inst_11 : Module B N] [inst_12 : IsScalarTower R B N] (n : Submodule B N) (x : M) (y : N),
  (TensorProduct.AlgebraTensorModule.tensorQuotientEquiv A B M n) (x ⊗ₜ[R] Submodule.Quotient.mk y) =
    Submodule.Quotient.mk (x ⊗ₜ[R] y)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.toList_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {f : α → Bool},
  (Std.TreeSet.filter f t).toList = List.filter f t.toList
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.comap_bracket_eq : ∀ {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] [inst_7 : LieRingModule L M₂] (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂)
  [inst_8 : LieAlgebra R L] [LieModule R L M₂] (I : LieIdeal R L) [LieModule R L M],
  f.ker = ⊥ → N₂ ≤ f.range → LieSubmodule.comap f ⁅I, N₂⁆ = ⁅I, LieSubmodule.comap f N₂⁆
-- Mathlib.Data.Nat.Factorization.Basic
/-- If the factorization of `n` contains just one number `p` then `n` is a power of `p`  -/
Nat.eq_pow_of_factorization_eq_single : ∀ {n p k : ℕ}, n ≠ 0 → (n.factorization = fun₀ | p => k) → n = p ^ k
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.HasPointwiseRightKanExtensionAt.eq_1 : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D),
  L.HasPointwiseRightKanExtensionAt F Y =
    CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_tprod_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (f : ι → M),
  ‖∏' (i : ι), f i‖₊ ≤ ⨆ i, ‖f i‖₊
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointIdIso_inv_app : ∀ {C₀ : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C₀] {F G : CategoryTheory.Functor C₀ C₀} (adj : F ⊣ G)
  (e : G ≅ CategoryTheory.Functor.id C₀) (X : C₀),
  (adj.leftAdjointIdIso e).inv.app X = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (e.hom.app (F.obj X))
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- The volume form on an oriented real inner product space, a nonvanishing top-dimensional
alternating form uniquely defined by compatibility with the orientation and inner product structure.
 -/
Orientation.volumeForm : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      {n : ℕ} → [_i : Fact (Module.finrank ℝ E = n)] → Orientation ℝ E (Fin n) → E [⋀^Fin n]→ₗ[ℝ] ℝ
-- Mathlib.Order.Max
OrderDual.noBotOrder : ∀ {α : Type u_1} [inst : LE α] [NoTopOrder α], NoBotOrder αᵒᵈ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.not_mem_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {a : α}, a ∉ Std.DTreeMap.Internal.Impl.empty
-- Mathlib.Order.Antichain
IsAntichain.image_relEmbedding_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ↪r r'},
  IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.addEquiv₀_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (a : X ⟶ Y),
  CategoryTheory.Abelian.Ext.addEquiv₀.symm a = CategoryTheory.Abelian.Ext.mk₀ a
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.neg.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (q : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.neg q =
    Quot.liftOn q
      (fun x =>
        match x with
        | (a, b) => Lean.Grind.IntModule.OfNatModule.Q.mk (b, a))
      ⋯
-- Mathlib.Order.Monotone.Basic
StrictMono.add_le_nat : ∀ {f : ℕ → ℕ}, StrictMono f → ∀ (m n : ℕ), m + f n ≤ f (m + n)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.map_arrow : ∀ {n : ℕ} {X Y : SSet.Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) (i : Fin m),
  (f.map σ).arrow i =
    (CategoryTheory.ConcreteCategory.hom (σ.app (Opposite.op { obj := { len := 1 }, property := ⋯ }))) (f.arrow i)
-- Init.Data.UInt.Lemmas
UInt16.neg_mul_not_eq_add_mul : ∀ {a b : UInt16}, -(a * ~~~b) = a + a * b
-- Init.Sym.Lemmas
Lean.Sym.Int16.le_eq_true : ∀ (a b : Int16), decide (a ≤ b) = true → (a ≤ b) = True
-- ProofWidgets.Component.HtmlDisplay
/-- Construct a structured message from ProofWidgets HTML.

For the meaning of `alt`, see `MessageData.ofWidget`.  -/
Lean.MessageData.ofHtml : ProofWidgets.Html → String → Lean.CoreM Lean.MessageData
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.finset_sup_comp : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (q : SeminormFamily 𝕜₂ F ι) (s : Finset ι)
  (f : E →ₛₗ[σ₁₂] F), (s.sup q).comp f = s.sup (q.comp f)
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_neg_one_lt_half : Real.exp (-1) < 1 / 2
-- Mathlib.Util.AtomM.Recurse
/-- Normalizes an expression, given initial data:

* `s`: a reference to the mutable `AtomM` state, for persisting across calls.
  This ensures that atom ordering is used consistently.
* `cfg`: the configuration options
* `wellBehavedDischarge` : MUST be set to `false` IF `eval` accesses local declarations with
  index >= `Context.lctxInitIndices`.
  Reason: it would cause `simp` to cache results too aggressively.
* `eval`: a normalization operation which will be run recursively, potentially dependent on a known
  atom ordering
* `simp`: a cleanup operation which will be used to post-process expressions
* `tgt`: the expression to normalize
 -/
Mathlib.Tactic.AtomM.recurse : IO.Ref Mathlib.Tactic.AtomM.State →
  Mathlib.Tactic.AtomM.Recurse.Config →
    Bool →
      (Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result) →
        (Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result) → Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Init.Data.Float.Model.Unpacked.Round
/-- Transforms a mantissa and an accuracy into an extended mantissa with the
residual bits initialized to represent the given accuracy.
 -/
Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy : ℕ → Float.Model.UnpackedFloat.Accuracy → Float.Model.UnpackedFloat.ExtendedMantissa
-- Std.Time.Duration
Std.Time.Duration.instDecidableLt : {x y : Std.Time.Duration} → Decidable (x < y)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k kmi : α},
  (t.insert k).min?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Lean.Data.KVMap
Lean.DataValue.sameCtor : Lean.DataValue → Lean.DataValue → Bool
-- Init.Data.Int.DivMod.Lemmas
Int.emod_bmod : ∀ (x : ℤ) (n : ℕ), (x % ↑n).bmod n = x.bmod n
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.zero : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Init.Data.Slice.List.Iterator
instSliceSizeListSliceData : {α : Type u} → Std.Slice.SliceSize (Std.Slice.Internal.ListSliceData α)
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [hw : w.GuitartExact] (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_one : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S), (Matrix.GeneralLinearGroup.map f) 1 = 1
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.mk.inj : ∀ {depth : ℕ} {commonFVarIds : Array Lean.FVarId} {goals : Array (Lean.MVarId × Array Lean.FVarId)} {depth_1 : ℕ}
  {commonFVarIds_1 : Array Lean.FVarId} {goals_1 : Array (Lean.MVarId × Array Lean.FVarId)},
  { depth := depth, commonFVarIds := commonFVarIds, goals := goals } =
      { depth := depth_1, commonFVarIds := commonFVarIds_1, goals := goals_1 } →
    depth = depth_1 ∧ commonFVarIds = commonFVarIds_1 ∧ goals = goals_1
-- Lean.DocString.Syntax
Lean.Doc.Syntax.list_item.quot : Lean.ParserDescr
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.closedBallAddSubgroup_top : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ⊤.closedBallAddSubgroup = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminal.comp_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P Q : C}
  (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.terminal.from Q) = CategoryTheory.Limits.terminal.from P
-- Mathlib.Order.Hom.Basic
OrderHom.compₘ_coe_coe_coe : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (x : β →o γ) (a : α →o β), ⇑((OrderHom.compₘ x) a) = ⇑x ∘ ⇑a
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_sum : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (n : ℕ)
  (f : ℕ → R → Polynomial S), (p.sum f).coeff n = p.sum fun a b => (f a b).coeff n
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_neg_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : NegZeroClass R] (x : HahnSeries Γ R),
  (-x).cardSupp ≤ x.cardSupp
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_multiset_prod : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (m : Multiset (Polynomial R)), Polynomial.map f m.prod = (Multiset.map (Polynomial.map f) m).prod
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.alternatingMapLinearEquiv_symm_map : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  exteriorPower.alternatingMapLinearEquiv.symm (exteriorPower.map n f) = (exteriorPower.ιMulti R n).compLinearMap f
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impTo : Lean.Parser.Parser
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int32.toBitVec_ite : ∀ {c : Prop} {t e : Int32} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.LinearAlgebra.Projection
/-- The linear map from `(p →ₗ[R₁] F) × (q →ₗ[R₁] F)` to `E →ₗ[R₁] F`.  -/
LinearMap.ofIsComplProd : {E : Type u_2} →
  [inst : AddCommGroup E] →
    {F : Type u_3} →
      [inst_1 : AddCommGroup F] →
        {R₁ : Type u_7} →
          [inst_2 : CommRing R₁] →
            [inst_3 : Module R₁ E] →
              [inst_4 : Module R₁ F] →
                {p q : Submodule R₁ E} → IsCompl p q → (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.Trivialization.mdifferentiableAt_snd_comp_iff₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E} {x₀ : M},
  f x₀ ∈ e.source →
    f x₀ ∈ e'.source →
      (MDiffAt fun x => (f x).proj) x₀ → ((MDiffAt fun x => (↑e (f x)).2) x₀ ↔ (MDiffAt fun x => (↑e' (f x)).2) x₀)
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instOrderBotOfOrderTop : (α : Type u) → [inst : LE α] → [h : OrderTop α] → OrderBot αᵒᵈ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α} {fallback : β} {c : ℕ},
  Std.DHashMap.Const.getD (Std.DHashMap.emptyWithCapacity c) a fallback = fallback
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveAt.hasMFDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ},
  IsMIntegralCurveAt γ v t₀ → HasMFDerivAt% γ t₀ (ContinuousLinearMap.smulRight 1 (v (γ t₀)))
-- Lean.Server.Requests
Lean.FileMap.rangeOverlapsRequestedRange : Lean.FileMap → Lean.Syntax.Range → Lean.Syntax.Range → optParam Bool false → optParam Bool false → Bool
-- Mathlib.Data.Matrix.Basic
Matrix.piLinearEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} (R : Type u_16) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → Module R (β i)] (a : (i : ι) → Matrix m n (β i)),
  (Matrix.piLinearEquiv R).symm a = Matrix.piAddEquiv.invFun a
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasurableEmbedding.setIntegral_map : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} {Y : Type u_5} {x : MeasurableSpace Y} {f : X → Y},
  MeasurableEmbedding f →
    ∀ (g : Y → E) (s : Set Y), ∫ (y : Y) in s, g y ∂MeasureTheory.Measure.map f μ = ∫ (x : X) in f ⁻¹' s, g (f x) ∂μ
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_comp : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] {C : Type u_2} [inst_5 : AddCommGroup C] [inst_6 : Module R C]
  (f : A →ₗ[R] B) (g : B →ₗ[R] C), CharacterModule.dual (g ∘ₗ f) = CharacterModule.dual f ∘ₗ CharacterModule.dual g
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGELE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ), t.IsGE ((t.truncGELE a b).obj X) a
-- Mathlib.Analysis.Real.Pi.Bounds
/-- Create a proof of `π < a` for a fixed rational number `a`, given a witness, which is a
sequence of rational numbers `√2 < r 1 < r 2 < ... < r n < 2` satisfying the property that
`√(2 + r i) ≥ r(i+1)`, where `r 0 = 0` and `√(2 - r n) ≤ (a - 1/4^n) / 2^(n+1)`.  -/
Real.«tacticPi_upper_bound[_,,]» : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Quotient
/-- Map sending an element of `M` to the corresponding element of `M ⧸ N`, when `N` is a
Lie submodule of the Lie module `M`.  -/
LieSubmodule.Quotient.mk : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → {N : LieSubmodule R L M} → M → M ⧸ N
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalars_extendScalarsOfSurjective : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[R] B),
  AlgEquiv.restrictScalars R ((AlgEquiv.extendScalarsOfSurjective h) f) = f
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f : CategoryTheory.Aut F) (A : C) [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj),
  (CategoryTheory.ConcreteCategory.hom
        (F.map
          ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ })
              (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F) f))).hom))
      a =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app A)) a
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTrivAt_apply_mk : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B)
  (a : F), ↑(Z.localTrivAt b) ⟨b, a⟩ = (b, a)
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_clog_helper : ∀ {b m n : ℕ}, Nat.blt 1 b = true → (b ^ m).blt n = true → n.ble (b ^ (m + 1)) = true → Nat.clog b n = m + 1