mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.continuousWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → ContinuousWithinAt f s x
-- Mathlib.Analysis.SpecialFunctions.Log.Monotone
Real.log_div_self_rpow_antitoneOn : ∀ {a : ℝ}, 0 < a → AntitoneOn (fun x => Real.log x / x ^ a) (Set.Ici (Real.exp a⁻¹))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Z) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).hom.app X_1).fst.app x =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj (V.obj (U.obj x)))
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimits F],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.Algebra.Free
/-- Associativity relations for a magma.  -/
Magma.AssocRel : (α : Type u) → [Mul α] → α → α → Prop
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- If `ζ ^ n = 1` and `ζ ≠ 1`, then `ζ - 1` divides `n`. This does not require `ζ` to be a
primitive root of unity, only a root of unity different from `1`.  -/
sub_one_dvd_natCast_of_pow_eq_one : ∀ {n : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A], ζ ^ n = 1 → ζ ≠ 1 → ζ - 1 ∣ ↑n
-- Mathlib.Order.Heyting.Basic
hnot_bot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α], ￢⊥ = ⊤
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The `Basis ι 𝕜 E` underlying the `OrthonormalBasis`  -/
OrthonormalBasis.toBasis : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] → [inst_3 : Fintype ι] → OrthonormalBasis ι 𝕜 E → Module.Basis ι 𝕜 E
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f g : β → α}
  (h₁ : s = t), (∀ x ∈ s, f x = g x) → s.sup' H f = t.sup' ⋯ g
-- Mathlib.ModelTheory.Graph
/-- The language consisting of a single relation representing adjacency.  -/
FirstOrder.Language.graph : FirstOrder.Language
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  {x y : d.Hom e}, x.h = y.h → x = y
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- For level `N = 1`, the gamma sets simplify to only a `gcd` condition.  -/
EisensteinSeries.gammaSet_one_eq : ∀ (r : ℕ) (a : Fin 2 → ZMod 1), EisensteinSeries.gammaSet 1 r a = {v | (v 0).gcd (v 1) = r}
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofFiniteGrp.eq_1 : ∀ (G : FiniteGrp.{u_1}), ProfiniteGrp.ofFiniteGrp G = ProfiniteGrp.of ↑G.toGrp
-- Mathlib.Data.Multiset.Fold
Multiset.fold_union_inter : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] [inst : DecidableEq α]
  (s₁ s₂ : Multiset α) (b₁ b₂ : α),
  op (Multiset.fold op b₁ (s₁ ∪ s₂)) (Multiset.fold op b₂ (s₁ ∩ s₂)) =
    op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.exists_isTuranMaximal : ∀ {V : Type u_1} [inst : Fintype V] {r : ℕ}, 0 < r → ∃ H x, H.IsTuranMaximal r
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁)
      (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) =
    CategoryTheory.CategoryStruct.comp
      (y.negOnePow •
        CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁'))
      h
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {s : Subring S} {f : R →+* S} {x : R},
  x ∈ Subring.comap f s ↔ f x ∈ s
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃),
  CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber g)
      (CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber f)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [inst : SMul R α] [inst_1 : SMul R β]
  (f : α → β) (r : R), (∀ (a : α), f (r • a) = r • f a) → ∀ (M : Matrix m n α), (r • M).map f = r • M.map f
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.uriTooLong.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.uriTooLong = 1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquiv.congr_simp : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (I : Ideal R) (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f f_1 : R ≃+* S) (e_f : f = f_1) (hIJ : J = Ideal.map (↑f) I),
  I.quotientEquiv J f hIJ = I.quotientEquiv J f_1 ⋯
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**, because it requires a balancing constraint on the inputs.

O(log n). Extract and remove the maximum element from a nonempty tree.  -/
Ordnode.splitMax' : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α × α
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul : ∀ (p : Polynomial ℝ) (x : ℝ),
  HasDerivAt (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (Polynomial.X ^ 2 * (p - Polynomial.derivative p)) * expNegInvGlue x) x
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- `g` is nonnegative  -/
AkraBazziRecurrence.g_nonneg : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r), ∀ x ≥ 0, 0 ≤ g x
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsDominant f],
  AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsDominant g
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.le_inf_support_coeff_multisetProd`. -/
AddMonoidAlgebra.le_inf_support_multiset_prod : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid T] [AddLeftMono T] [AddRightMono T] {degt : A → T},
  0 ≤ degt 0 →
    (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
      ∀ (m : Multiset (AddMonoidAlgebra R A)),
        (Multiset.map (fun f => f.coeff.support.inf degt) m).sum ≤ m.prod.coeff.support.inf degt
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_smul_left : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (α : ℝ),
  ProbabilityTheory.mgf (α • X) μ t = ProbabilityTheory.mgf X μ (α * t)
-- Init.Data.Vector.Range
Vector.range_succ_eq_map : ∀ {n : ℕ}, Vector.range (n + 1) = Vector.cast ⋯ (#v[0] ++ Vector.map Nat.succ (Vector.range n))
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryGT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → α → α × β
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.inv_left_hom_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L R} (e : Y ⟶ X) [inst_3 : CategoryTheory.IsIso e],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.inv e.left)) Y.hom)
      (R.map e.right) =
    X.hom
-- Mathlib.Analysis.Convex.Strong
uniformConcaveOn_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
  UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_normal : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore.Normal
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- A family of measurable equivalences `Π a, β₁ a ≃ᵐ β₂ a` generates a measurable equivalence
between `Π a, β₁ a` and `Π a, β₂ a`.  -/
MeasurableEquiv.piCongrRight : {δ' : Type u_5} →
  {π : δ' → Type u_6} →
    {π' : δ' → Type u_7} →
      [inst : (x : δ') → MeasurableSpace (π x)] →
        [inst_1 : (x : δ') → MeasurableSpace (π' x)] → ((a : δ') → π a ≃ᵐ π' a) → ((a : δ') → π a) ≃ᵐ ((a : δ') → π' a)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selRightfAction_actionHom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {c c' d d' : C} (f : d ⟶ d') (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f g
-- Mathlib.Order.Category.Frm
_private.Mathlib.Order.Category.Frm.0.Frm.Hom.mk.injEq : ∀ {X Y : Frm} (hom' hom'_1 : FrameHom ↑X ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom_ext : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (f g : X ⟶ Y),
  CategoryTheory.Arrow.Hom.left f = CategoryTheory.Arrow.Hom.left g →
    CategoryTheory.Arrow.Hom.right f = CategoryTheory.Arrow.Hom.right g → f = g
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- A more bundled version of `AffineEquiv.constVAdd`.  -/
AffineEquiv.constVAddHom : (k : Type u_1) →
  (P₁ : Type u_2) →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → Multiplicative V₁ →* P₁ ≃ᵃ[k] P₁
-- Lean.DocString.Parser
/-- Parses a block quote.  -/
Lean.Doc.Parser.blockquote : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.List.Rotate
List.isRotated_cyclicPermutations_iff : ∀ {α : Type u} {l l' : List α}, l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'
-- Init.Data.Nat.Basic
Nat.not_add_one_le_self : ∀ (n : ℕ), ¬n + 1 ≤ n
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.mul_star_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(pinGroup Q)), x * star x = 1
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.Consumer.promise : {α : Type} → Std.CloseableChannel.Bounded.Consumer✝ α → IO.Promise Bool
-- Mathlib.NumberTheory.Padics.Complex
/-- The valuation on `ℂ_[p]` extends the valuation on `PadicAlgCl p`.  -/
PadicComplex.valuation_extends : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), Valued.v ↑x = Valued.v x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} {hc : k' ∈ Std.DTreeMap.Raw.Const.modify t k f},
  (Std.DTreeMap.Raw.Const.modify t k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.right_mem_of_mem_openSegment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E} {x : E},
  IsExtreme 𝕜 A B → ∀ {y z : E}, x ∈ A → y ∈ A → z ∈ B → z ∈ openSegment 𝕜 x y → y ∈ B
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.of_card_le_one : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G},
  A.Nonempty → B.Nonempty → A.card ≤ 1 → B.card ≤ 1 → ∃ a ∈ A, ∃ b ∈ B, UniqueAdd A B a b
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_series_eq_iff : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) [Nontrivial E] (c' : ℕ → 𝕜),
  FormalMultilinearSeries.ofScalars E c = FormalMultilinearSeries.ofScalars E c' ↔ c = c'
-- Mathlib.Data.Set.Function
/-- **Alias** of `Set.image_sdiff_of_injOn`.

---

**Alias** of `Set.InjOn.image_sdiff_subset`. -/
Set.image_diff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set α},
  Set.InjOn f s → t ⊆ s → f '' (s \ t) = f '' s \ f '' t
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.op_eq_self_of_isPrincipal : ∀ {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  a < o → Order.IsNormal (op a) → Ordinal.IsPrincipal op o → Order.IsSuccLimit o → op a o = o
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).unitIso.hom.app X).f =
    CategoryTheory.CategoryStruct.id X.a
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.absolutelyContinuous : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.HasPDF X ℙ μ],
  (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.lid_tmul : ∀ {R : Type u_1} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Bialgebra R B] (r : R) (a : B),
  (Bialgebra.TensorProduct.lid R B) (r ⊗ₜ[R] a) = r • a
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν → ∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun b => f (a, b) q) (ν a)
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `M` is a free module, then so is its `n`th exterior power.  -/
exteriorPower.instFree : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Free R M], Module.Free R ↥(⋀[R]^n M)
-- Lean.Meta.Basic
/-- If `true`, reduce recursor/matcher applications, e.g., `Nat.rec true (fun _ _ => false) Nat.zero` reduces to `true`  -/
Lean.Meta.Config.iota : Lean.Meta.Config → Bool
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.zero_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C D : HomologicalComplex V c) (i : ι),
  HomologicalComplex.Hom.f 0 i = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftIso_hom : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ'),
  (CategoryTheory.Limits.CatCospanTransform.leftIso e).hom = e.hom.left
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.opParallelPairIso_hom_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.opParallelPairIso f g).hom.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.parallelPair f g).op.obj (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one))
-- Init.Data.Vector.Lemmas
Vector.eraseIdx.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n),
  xs = xs_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (h : i < n), xs.eraseIdx i h = xs_1.eraseIdx i_1 ⋯
-- Mathlib.Algebra.Lie.Weights.IsSimple
_private.Mathlib.Algebra.Lie.Weights.IsSimple.0.LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_aux : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H)),
  (∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)) →
    ∀ (χ : LieModule.Weight K (↥H) L) (x_χ m_α : L),
      x_χ ∈ LieModule.genWeightSpace L ⇑χ →
        ∀ (α : LieModule.Weight K (↥H) L),
          LieModule.Weight.toLinear K (↥H) L α ∈ q →
            ∀ (hα₀ : α.IsNonZero),
              m_α ∈ LieAlgebra.IsKilling.sl2SubmoduleOfRoot hα₀ →
                ⁅x_χ, m_α⁆ ∈ ⨆ α, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_sup : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (m m' : MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.map f) (m ⊔ m') =
    (MeasureTheory.OuterMeasure.map f) m ⊔ (MeasureTheory.OuterMeasure.map f) m'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.length_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.WF → t.toList.length = t.size
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckExplicit : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The vector field at any time is Lipschitz with constant `K` within a closed ball.  -/
IsPicardLindelof.lipschitzOnWith : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K → ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith K (f t) (Metric.closedBall x₀ ↑a)
-- Mathlib.Order.CompleteLattice.Basic
Monotone.map_sInf_le : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {s : Set α} {f : α → β},
  Monotone f → f (sInf s) ≤ ⨅ a ∈ s, f a
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (k : C)
  {X Y : C} (f : X ⟶ Y) (X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' C).obj k).map f).app X₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X k X₃).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f k) X₃)
        (CategoryTheory.MonoidalCategoryStruct.associator Y k X₃).hom)
-- Mathlib.GroupTheory.GroupAction.Quotient
QuotientGroup.out_conj_pow_minimalPeriod_mem : ∀ {G : Type u} [inst : Group G] (H : Subgroup G) (g : G) (q : G ⧸ H),
  (Quotient.out q)⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q * Quotient.out q ∈ H
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup_dite_pos : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} (p : β → Prop)
  [inst_2 : DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β},
  b ∈ s → ∀ (h₁ : p b), f b h₁ ≤ s.sup fun i => if h : p i then f i h else g i h
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) =
    FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
        FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      (hζ.toInteger - 1) *
        FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_fg : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  Function.Injective ⇑(algebraMap R P) → ∀ (I : Ideal R), (↑↑I).FG ↔ I.FG
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Implementation; see `StructuredArrow.prodEquivalence`.  -/
CategoryTheory.StructuredArrow.prodInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (S : D) →
                  (S' : D') →
                    (T : CategoryTheory.Functor C D) →
                      (T' : CategoryTheory.Functor C' D') →
                        CategoryTheory.Functor
                          (CategoryTheory.StructuredArrow S T × CategoryTheory.StructuredArrow S' T')
                          (CategoryTheory.StructuredArrow (S, S') (T.prod T'))