mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- For any trivialization `e`, the smoothness of a `C^n` section on `e.baseSet`
can be determined using `e`.  -/
Bundle.Trivialization.contMDiffOn_section_baseSet_iff : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [MemTrivializationAtlas e],
  ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) e.baseSet ↔
    ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑e ⟨x, s x⟩).2) e.baseSet
-- Lean.AuxRecursor
Lean.markSparseCasesOn : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.integrable_pow_mul_iteratedFDeriv : ∀ {D : Type u_4} {V : Type u_9} [inst : NormedAddCommGroup D] [inst_1 : NormedSpace ℝ D] [inst_2 : NormedAddCommGroup V]
  [inst_3 : NormedSpace ℝ V] [inst_4 : MeasurableSpace D] (μ : MeasureTheory.Measure D) [hμ : μ.HasTemperateGrowth]
  [BorelSpace D] [SecondCountableTopology D] (f : SchwartzMap D V) (k n : ℕ),
  MeasureTheory.Integrable (fun x => ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) μ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roc_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m<...=n).toList[i]? = some k ↔ i < (n - m).toNat ∧ m + 1 + ↑i = k
-- Init.Data.Array.Lemmas
Array.size_range : ∀ {n : ℕ}, (Array.range n).size = n
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → Λ)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.goto a with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_6 (Turing.TM2.Stmt.goto a) a ⋯
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mk_surjective : ∀ {α : Type u} [inst : AddMonoid α], Function.Surjective AddConjClasses.mk
-- Mathlib.Order.Category.Preord
Preord.coe_of : ∀ (X : Type u) [inst : Preorder X], ↑{ carrier := X, str := inst } = X
-- Init.Data.List.Monadic
List.flatMapM.loop.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x : List α)
  (x_1 : List (List β)),
  List.flatMapM.loop f x x_1 =
    match x, x_1 with
    | [], bs => pure bs.reverse.flatten
    | a :: as, bs => do
      let bs' ← f a
      List.flatMapM.loop f as (bs' :: bs)
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.add_liftRight_neg : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N)
  (h : ∀ (x : M), IsAddUnit (f x)) (x : M), f x + ↑(-(IsAddUnit.liftRight f h) x) = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denoteAsIntModule_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p = Lean.Grind.CommRing.Poly.denote ctx p
-- Lean.Elab.ParseImportsFast
Lean.printImportsJson : Array String → IO Unit
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
are dense. Formulated here with an index set which is a countable type.  -/
dense_iUnion_interior_of_closed : ∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X},
  (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → Dense (⋃ i, interior (f i))
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.toUpper_symm : ∀ {α : Type u_3}, Topology.WithUpper.toUpper.symm = Topology.WithUpper.ofUpper
-- Init.Data.Int.DivMod.Lemmas
Int.lt_fdiv_add_one_mul_self : ∀ (a : ℤ) {b : ℤ}, 0 < b → a < (a.fdiv b + 1) * b
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorial_succ : ∀ {n k : ℕ}, n.ascFactorial k.succ = (n + k) * n.ascFactorial k
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_mul_self : ∀ {x : ℝ}, Irrational (x * x) → Irrational x
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffWithinAt.coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_20 : MemTrivializationAtlas e] [inst_21 : MemTrivializationAtlas e'] {s : Set M} {f : M → B} {x : M},
  ContMDiffWithinAt IM IB n f s x →
    f x ∈ e.baseSet →
      f x ∈ e'.baseSet →
        ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n
          (fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))) s x
-- Init.Data.List.Count
List.countP.go.eq_1 : ∀ {α : Type u} (p : α → Bool) (a : ℕ), List.countP.go p [] a = a
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCodetecting.isIso_iff_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsCodetecting →
    ∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
      CategoryTheory.IsIso f ↔
        ∀ (G : C),
          P G → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yoneda.obj G).map f.op))
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulPointed.eq_1 : ∀ {G : Type u_1} [inst : Group G] (M : Submonoid G), M.IsMulPointed = ∀ x ∈ M, x⁻¹ ∈ M → x = 1
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Ioc_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.Ioc i.succ j.succ = Set.Ioc i j
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.instHasStrictTerminalObjectsOfIsThin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [Quiver.IsThin C],
  CategoryTheory.Limits.HasStrictTerminalObjects C
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForDiagnosticsParams.fromJson : Lean.Json → Except String Lean.Lsp.WaitForDiagnosticsParams
-- Mathlib.Order.CompleteLattice.Defs
instCompleteSemilatticeSupOrderDualOfCompleteSemilatticeInf.eq_1 : ∀ {α : Type u_8} [inst : CompleteSemilatticeInf α],
  instCompleteSemilatticeSupOrderDualOfCompleteSemilatticeInf =
    { toPartialOrder := OrderDual.instPartialOrder α, toSupSet := OrderDual.supSet α, isLUB_sSup := ⋯ }
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for strict monotonicity of scalar multiplication by positive elements on the left,
namely `b₁ < b₂ → a • b₁ < a • b₂` if `0 < a`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
PosSMulStrictMono : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → Prop
-- Mathlib.Order.Filter.Map
Filter.bind_le : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : α → Filter β} {l : Filter β},
  (∀ᶠ (x : α) in f, g x ≤ l) → f.bind g ≤ l
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.inv.inj : ∀ {R : Type u} {a a_1 : Rack.PreEnvelGroup R}, a.inv = a_1.inv → a = a_1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomain_sub : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] {p : ι → Prop} [inst_1 : DecidablePred p]
  {v v' : Π₀ (i : ι), β i}, DFinsupp.subtypeDomain p (v - v') = DFinsupp.subtypeDomain p v - DFinsupp.subtypeDomain p v'
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.finite_primeSpectrum : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Finite (PrimeSpectrum R)] [Algebra.QuasiFinite R S], Finite (PrimeSpectrum S)
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_le_min_of_subset : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty},
  s ⊆ t → ht.min htn ≤ hs.min hsn
-- Mathlib.Order.Atoms
/-- **Alias** of `exists_covBy_le_of_lt`. -/
LT.lt.exists_covby_le : ∀ {α : Type u_4} {a b : α} [inst : Preorder α] [IsStronglyAtomic α], a < b → ∃ x, a ⋖ x ∧ x ≤ b
-- Init.Data.String.Basic
String.sliceFrom_toSlice : ∀ {s : String} {p : s.Pos}, s.toSlice.sliceFrom p.toSlice = s.sliceFrom p
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Hom.of : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ → CategoryTheory.Pseudofunctor.StrongTrans.Hom η θ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs c =
      Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs c_1 →
    c = c_1
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref : Sort u_1 → Sort (max 1 u_1)
-- Std.Sync.SharedMutex
/-- Unlocks a `BaseSharedMutex` write lock.

The current thread must have already locked the mutex for write access.
Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseSharedMutex.unlockWrite : Std.BaseSharedMutex → BaseIO Unit
-- Mathlib.Data.Finset.Defs
List.instDecidableSurjOnCoeFinsetOfDecidableEq : {α : Type u_1} →
  {β : Type u_2} → {f : α → β} → {s : Finset α} → {t' : Finset β} → [DecidableEq β] → Decidable (Set.SurjOn f ↑s ↑t')
-- Mathlib.Order.Filter.Pointwise
Filter.instNeg.eq_1 : ∀ {α : Type u_2} [inst : Neg α], Filter.instNeg = { neg := Filter.map Neg.neg }
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (F.mapShortComplex.obj S₁).HasHomology]
  [inst_8 : (F.mapShortComplex.obj S₂).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂]
  [CategoryTheory.ShortComplex.QuasiIso φ], CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ)
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C} {n : ℤ}
  (f : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n),
  (CategoryTheory.ShiftedHom.opEquiv n).symm f =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop
      ((CategoryTheory.shiftFunctor C n).map (Quiver.Hom.unop f))
-- Lean.Parser.Basic
Lean.Parser.dbgTraceStateFn : String → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Combinatorics.Derangements.Basic
/-- For any `a : α`, the fiber over `some a` is the set of permutations
where `a` is the only possible fixed point.  -/
derangements.Equiv.RemoveNone.fiber_some : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α),
  derangements.Equiv.RemoveNone.fiber (some a) = {f | Function.fixedPoints ⇑f ⊆ {a}}
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.ennrealToMeasure_zero : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasureTheory.VectorMeasure.ennrealToMeasure 0 = 0
-- Mathlib.CategoryTheory.FintypeCat
/-- Given any natural number `n`, this creates the associated object of `FintypeCat.Skeleton`.  -/
FintypeCat.Skeleton.mk : ℕ → FintypeCat.Skeleton
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} {hF : eA.functor.comp e'.functor ≅ F} {G : CategoryTheory.Functor B A}
  {hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor} {η : G.comp F ≅ eB.functor},
  AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ hF hG η →
    (AlgebraicTopology.DoldKan.Compatibility.equivalence hF hG).counitIso =
      AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso η
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Comon C), M.id.hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (Topology.WithLawson α)
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- Given a finite type `α` and a function `f : α → ℝ≥0∞` with sum 1, we get a `PMF`.  -/
PMF.ofFintype : {α : Type u_1} → [inst : Fintype α] → (f : α → ENNReal) → ∑ a, f a = 1 → PMF α
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_le_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t → ∀ (u : Multiset α), u ∪ s ≤ u ∪ t
-- Batteries.Data.Vector.Lemmas
Vector.getElem?_scanr_zero : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as)[0]? = some (Vector.foldr f init as)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₄ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  {φ φ' : f ⟶ g},
  CategoryTheory.ComposableArrows.app' φ 0 _proof_361✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_361✝ →
    CategoryTheory.ComposableArrows.app' φ 1 _proof_362✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_362✝ →
      CategoryTheory.ComposableArrows.app' φ 2 _proof_363✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_363✝ →
        CategoryTheory.ComposableArrows.app' φ 3 _proof_364✝ = CategoryTheory.ComposableArrows.app' φ' 3 _proof_364✝ →
          CategoryTheory.ComposableArrows.app' φ 4 _proof_365✝ = CategoryTheory.ComposableArrows.app' φ' 4 _proof_365✝ →
            φ = φ'
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Measurable.comp_aemeasurable' : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} [inst : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : MeasurableSpace δ] {f : α → δ} {g : δ → β},
  Measurable g → AEMeasurable f μ → AEMeasurable (fun x => g (f x)) μ
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.map_id : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] (P : Submonoid A),
  HomogeneousLocalization.map (GradedRingHom.id 𝒜) ⋯ = RingHom.id (HomogeneousLocalization 𝒜 P)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f f_1 : A₁ ⟶ B) (e_f : f = f_1)
  (g g_1 : A₂ ⟶ B) (e_g : g = g_1) [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.Subobject.ofMkLEMk f g h = CategoryTheory.Subobject.ofMkLEMk f_1 g_1 ⋯
-- Init.Data.BitVec.Bitblast
/-- Shifts `x` logically to the right by the first `n` bits of `y`.

The theorem `BitVec.shiftRight_eq_ushiftRightRec` proves the equivalence
of `(x >>> y)` and `BitVec.ushiftRightRec`.

Together with equations `BitVec.ushiftRightRec_zero` and `BitVec.ushiftRightRec_succ`,
this allows `BitVec.ushiftRight` to be unfolded into a circuit for bit blasting.
 -/
BitVec.ushiftRightRec : {w₁ w₂ : ℕ} → BitVec w₁ → BitVec w₂ → ℕ → BitVec w₁
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mulInvariantVectorField_eq_mpullback : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I (minSmoothness 𝕜 3) G]
  (g : G) (V : (g : G) → TangentSpace I g),
  mulInvariantVectorField (V 1) g = VectorField.mpullback I I (fun x => g⁻¹ * x) V g
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
/-- The comparison isomorphism between `normalizedMooreComplex A` and
the functor `Idempotents.DoldKan.N` from the pseudoabelian case  -/
CategoryTheory.Abelian.DoldKan.comparisonN : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] → CategoryTheory.Abelian.DoldKan.N ≅ CategoryTheory.Idempotents.DoldKan.N
-- Mathlib.Algebra.Order.Hom.Basic
GroupSeminormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Group α] [inst_1 : AddCommMonoid β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [toMulLEAddHomClass : MulLEAddHomClass F α β],
  (∀ (f : F), f 1 = 0) → (∀ (f : F) (a : α), f a⁻¹ = f a) → GroupSeminormClass F α β
-- Mathlib.Tactic.CongrExclamation
CongrState.mk.inj : ∀ {goals : Array Lean.MVarId} {patterns : List (Lean.TSyntax `rintroPat)} {goals_1 : Array Lean.MVarId}
  {patterns_1 : List (Lean.TSyntax `rintroPat)},
  { goals := goals, patterns := patterns } = { goals := goals_1, patterns := patterns_1 } →
    goals = goals_1 ∧ patterns = patterns_1
-- Mathlib.RingTheory.Unramified.Locus
Algebra.unramified_iff_forall : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FiniteType R A], Algebra.Unramified R A ↔ ∀ (q : PrimeSpectrum A), Algebra.IsUnramifiedAt R q.asIdeal
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.isBigO_cocompact_rpow : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) [ProperSpace E] (s : ℝ), ⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ s
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.mk.sizeOf_spec : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid G] {C : Set (Set α)} [inst_1 : SizeOf α] [inst_2 : SizeOf G]
  [inst_3 : (a : Set α) → SizeOf (C a)] (toFun : Set α → G) (empty' : toFun ∅ = 0)
  (sUnion' : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun (⋃₀ ↑I) = ∑ u ∈ I, toFun u),
  sizeOf { toFun := toFun, empty' := empty', sUnion' := sUnion' } = 1 + sizeOf empty'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.getKey! a = (t.getKey? a).get!
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          HomotopicalAlgebra.FibrantBrownFactorization f →
            (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.toBiheytingAlgebra : {α : Type u_1} → [self : CompleteDistribLattice α] → BiheytingAlgebra α
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (toCompacts : TopologicalSpace.Compacts α)
  (interior_nonempty' : (interior toCompacts.carrier).Nonempty) (toCompacts_1 : TopologicalSpace.Compacts α)
  (interior_nonempty'_1 : (interior toCompacts_1.carrier).Nonempty),
  ({ toCompacts := toCompacts, interior_nonempty' := interior_nonempty' } =
      { toCompacts := toCompacts_1, interior_nonempty' := interior_nonempty'_1 }) =
    (toCompacts = toCompacts_1)
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.center_eq_inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x : P} {R : ℝ}, R ≠ 0 → (c = EuclideanGeometry.inversion c R x ↔ x = c)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α},
  (Std.ExtTreeMap.filterMap f t)[k]! = (t[k]?.pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_left_inj : ∀ {R : Type u} [inst : Semiring R] {a : R},
  a ≠ 0 → ∀ {i j : ℕ}, (Polynomial.monomial i) a = (Polynomial.monomial j) a ↔ i = j
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {g : FrameHom β γ} {f₁ f₂ : FrameHom α β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Data.Set.Image
Set.preimage_const_of_mem : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : Set β}, b ∈ s → (fun x => b) ⁻¹' s = Set.univ
-- Mathlib.Data.Set.Inclusion
Set.coe_inclusion : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t) (x : ↑s), ↑(Set.inclusion h x) = ↑x