mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullback_obj_obj_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {Z : C} {f : X ⟶ Y} {F : TopCat.Presheaf C Y} (U : (TopologicalSpace.Opens ↑X)ᵒᵖ)
  {φ ψ : ((TopCat.Presheaf.pullback C f).obj F).obj U ⟶ Z},
  (∀ (V : TopologicalSpace.Opens ↑Y) (hV : Opposite.unop U ≤ (TopologicalSpace.Opens.map f).obj V),
      CategoryTheory.CategoryStruct.comp
          (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
          (CategoryTheory.CategoryStruct.comp
            (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) φ) =
        CategoryTheory.CategoryStruct.comp
          (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op V))
          (CategoryTheory.CategoryStruct.comp
            (((TopCat.Presheaf.pullback C f).obj F).map (CategoryTheory.homOfLE hV).op) ψ)) →
    φ = ψ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  (Std.DHashMap.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Const.get m k h) = true
-- Mathlib.LinearAlgebra.Matrix.StdBasis
/-- The standard basis of `Matrix m n R`.  -/
Matrix.stdBasis : (R : Type u_1) →
  (m : Type u_2) →
    (n : Type u_3) → [Fintype m] → [Finite n] → [inst : Semiring R] → Module.Basis (m × n) R (Matrix m n R)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept_zero_zero : ∀ (L : PeriodPair), L.derivWeierstrassPExcept 0 0 = 0
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_p_zpow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℤ), ‖↑p ^ n‖ = ↑p ^ (-n)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalAddGroup.uniformCauchySeqOn_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddGroup G] [u : UniformSpace G]
  [inst_1 : IsTopologicalAddGroup G] (F : ι → α → G) (p : Filter ι) (s : Set α),
  IsTopologicalAddGroup.rightUniformSpace G = u →
    (UniformCauchySeqOn F p s ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a - F m.1 a ∈ u_1)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E},
  t ∈ nhds x → VectorField.lieBracketWithin 𝕜 V W (s ∩ t) x = VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.rightUnitor_hom_toNatTrans : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C),
  (CategoryTheory.Bicategory.rightUnitor F).hom.toNatTrans = F.toFunctor.rightUnitor.hom
-- Mathlib.Algebra.Order.Floor.Ring
Int.natCast_mul_floor_div_cancel : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] {n : ℕ},
  n ≠ 0 → ∀ (a : R), ⌊↑n * a⌋ / ↑n = ⌊a⌋
-- Plausible.Functions
/-- Data structure specifying a total function using a list of pairs
and a default value returned when the input is not in the domain of
the partial function.

`withDefault f y` encodes `x => f x` when `x ∈ f` and `x => y`
otherwise.

We use `Σ` to encode mappings instead of `×` because we
rely on the association list API defined in `Mathlib/Data/List/Sigma.lean`.
  -/
Plausible.TotalFunction : Type u → Type v → Type (max u v)
-- Lean.Declaration
Lean.instInhabitedOpaqueVal.default : Lean.OpaqueVal
-- Init.Data.List.Lemmas
List.replace_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b c : α}, [a].replace b c = [if (b == a) = true then c else a]
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.topologicalSpace_eq : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)),
  UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Algebra.IsIntegral.mk : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  (∀ (x : A), IsIntegral R x) → Algebra.IsIntegral R A
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.hom_ext : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G) →
    ∀ (hG : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X}
      {s : CategoryTheory.Limits.Multifork (S.index G)} {f₁ f₂ : s.pt ⟶ G.obj (Opposite.op X)},
      (∀ (a : S.Arrow),
          CategoryTheory.CategoryStruct.comp f₁ (G.map a.f.op) = CategoryTheory.CategoryStruct.comp f₂ (G.map a.f.op)) →
        f₁ = f₂
-- Init.Grind.Config
/-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split.  -/
Lean.Grind.Config.ematch : Lean.Grind.Config → ℕ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{w + 1}}, Std.DHashMap.Raw.forM (fun a x => f a) ↑m = (↑m).keys.forM f
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquiv.toMonoidWithZeroHom_injective : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] (f : G ≃* H),
  Function.Injective ⇑f.toMonoidWithZeroHom
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_of_reducedToUnit : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l →
    ∀ (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p assignment →
        Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- Converting a bundled monoid to a monoid object in `Type`.
 -/
MonTypeEquivalenceMon.inverse : CategoryTheory.Functor MonCat (CategoryTheory.Mon (Type u))
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymExtension.mkInitial : {σ : Type} → Lean.Meta.Sym.SymExtension σ → IO σ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X), CategoryTheory.Sieve.pullback f ⊥ = ⊥
-- Mathlib.Topology.Separation.Hausdorff
limUnder_nhds_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] (x : X), (nhds x).limUnder id = x
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Millisecond.Offset.toNanoseconds : Std.Time.Millisecond.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B)
  {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A)
  {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)}
  (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [inst_3 : J.HasSheafCompose F],
  J.PreservesSheafification F ↔ CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `mul_left_cancel`. -/
mul_left_cancel'' : ∀ {G : Type u_1} [inst : Mul G] [IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
-- Std.Http.Protocol.H1
/-- Execute one step of the state machine.
 -/
Std.Http.Protocol.H1.Machine.step : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Std.Http.Protocol.H1.StepResult dir
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instFullPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.forget R).Full
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.mk : Lean.Syntax → Lean.Expr → Lean.Elab.Term.ExprWithHoles✝
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLift_p1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s)
      (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) =
    s.fst
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul_nc.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (pw : Lean.Grind.CommRing.Power)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit))
  (h_3 :
    (pw : Lean.Grind.CommRing.Power) → (m₁ : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult pw m₁)),
  (match Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit with
    | Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => h_2 pw
    | Lean.Grind.CommRing.Mon.mult pw m₁ => h_3 pw m₁) =
    h_2 pw
-- Init.Data.BitVec.Lemmas
BitVec.neg_sub : ∀ {w : ℕ} {x y : BitVec w}, -(x - y) = -x + y
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.zero_oreDiv' : ∀ {R : Type u_1} [inst : MonoidWithZero R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (s : ↥S), 0 /ₒ s = 0
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.natDegree_eraseLead_add_one : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.nextCoeff ≠ 0 → f.eraseLead.natDegree + 1 = f.natDegree
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.discreteUniformity_iff : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α],
  DiscreteUniformity (TopologicalSpace.Closeds α) ↔ DiscreteUniformity α
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) {β : ι → Type u_3} [m : (x : ι) → MeasurableSpace (β x)] (f : (x : ι) → Ω → β x)
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndepFun m' hm' f μ =
    ProbabilityTheory.Kernel.iIndepFun f (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.nonempty_of_measureReal_ne_zero : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ.real s ≠ 0 → s.Nonempty
-- Mathlib.Algebra.Opposites
/-- Multiplicative opposite of a type.  -/
«term_ᵐᵒᵖ» : Lean.TrailingParserDescr
-- Mathlib.Data.Finset.Powerset
/-- Variant of `Finset.image_injOn_powerset_of_injOn` for a family `S` of finsets whose
union supports an `InjOn` hypothesis, rather than the full powerset of a set.  -/
Finset.injOn_image_of_biUnion_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {S : Finset (Finset α)} {f : α → β},
  Set.InjOn f ↑(S.biUnion id) → Set.InjOn (fun x => Finset.image f x) ↑S
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.brecOn : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n →. ℕ) → Nat.Partrec' a → Prop} {n : ℕ} {a : List.Vector ℕ n →. ℕ}
  (t : Nat.Partrec' a),
  (∀ {n : ℕ} (a : List.Vector ℕ n →. ℕ) (t : Nat.Partrec' a), Nat.Partrec'.below t → motive a t) → motive a t
-- Mathlib.Data.List.Sigma
List.lookupAll_cons_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β),
  a ≠ s.fst → List.lookupAll a (s :: l) = List.lookupAll a l
-- Init.Data.Nat.Gcd
Nat.gcd_self_add_right : ∀ (m n : ℕ), m.gcd (m + n) = m.gcd n
-- Mathlib.Order.Filter.Pointwise
/-- `pure` as a `ZeroHom`.  -/
Filter.pureZeroHom : {α : Type u_2} → [inst : Zero α] → ZeroHom α (Filter α)
-- Mathlib.RingTheory.WittVector.Compare
WittVector.toPadicInt_comp_fromPadicInt_ext : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℤ_[p]),
  ((WittVector.toPadicInt p).comp (WittVector.fromPadicInt p)) x = (RingHom.id ℤ_[p]) x
-- Mathlib.Topology.Irreducible
exists_preirreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  IsPreirreducible s → ∃ t, IsPreirreducible t ∧ s ⊆ t ∧ ∀ (u : Set X), IsPreirreducible u → t ⊆ u → u = t
-- Mathlib.Algebra.Divisibility.Basic
Dvd.intro_left : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y),
  J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f
-- Init.Data.Array.Monadic
Array.idRun_forIn'_yield_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β),
  (forIn' xs init fun a m b => ForInStep.yield <$> f a m b).run =
    Array.foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => (f a h b).run)
      init xs.attach
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset : {A B : GrpCat} →
  {f : A ⟶ B} → ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range) → GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f
-- Std.Async.System
Std.Async.System.instInhabitedGroupId.default : Std.Async.System.GroupId
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_one : ∀ {α : Type u_2} {x y : α}, Equiv.Perm.SameCycle 1 x y ↔ x = y
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSets_piiUnionInter_of_disjoint : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {S T : Set ι},
  ProbabilityTheory.iCondIndepSets m' hm' s μ →
    Disjoint S T → ProbabilityTheory.CondIndepSets m' hm' (piiUnionInter s S) (piiUnionInter s T) μ
-- Mathlib.Algebra.Field.Basic
one_add_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {a b : K}, b ≠ 0 → 1 + a / b = (b + a) / b
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0_k_cons : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s).erase0_k =
    Bool.rec
      (Bool.rec (Lean.Grind.AC.Seq.cons x s.erase0_k) (Lean.Grind.AC.Seq.var x)
        (s.erase0_k.beq' (Lean.Grind.AC.Seq.var 0)))
      s.erase0_k (Nat.beq x 0)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_add : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f g : N →ₗ[R] P), LinearMap.lTensor M (f + g) = LinearMap.lTensor M f + LinearMap.lTensor M g
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.mem_fundamentalFrontier : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {x : α},
  x ∈ MeasureTheory.fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_some_getD_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.contains a = true → m.get? a = some (m.getD a fallback)
-- Mathlib.GroupTheory.Congruence.Basic
Con.comap_conGen_of_bijective : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M → N),
  Function.Bijective f →
    ∀ (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop),
      Con.comap f H (conGen rel) = conGen fun x y => rel (f x) (f y)
-- Mathlib.RingTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of rings commutes.  -/
RingCon.lift_comp_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (H : c ≤ RingCon.ker f), (c.lift f H).comp c.mk' = f
-- Mathlib.Order.Concept
Concept.le_ofObjects_of_extent_subset : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {c : Concept α β r},
  c.extent ⊆ s → c ≤ Concept.ofObjects r s
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra' : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : Field K] [inst_3 : CharZero K] [inst_4 : AddCommGroup M] [inst_5 : Module K M] [inst_6 : AddCommGroup N]
  [inst_7 : Module K N] {P : RootPairing ι K M N} [P.IsReduced] [inst_9 : P.IsCrystallographic] [P.IsIrreducible]
  [P.IsRootSystem] (b : P.Base), (RootPairing.GeckConstruction.cartanSubalgebra' b).IsCartanSubalgebra
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality : ∀ {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] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesLeftHomologyOf S₁] [inst_10 : F.PreservesLeftHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso F).inv =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).inv
      (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.beq.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (as : List α) (b : α) (bs : List α)
  (h_1 : Unit → motive [] []) (h_2 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs))
  (h_3 : (x x_1 : List α) → motive x x_1),
  (match a :: as, b :: bs with
    | [], [] => h_1 ()
    | a :: as, b :: bs => h_2 a as b bs
    | x, x_1 => h_3 x x_1) =
    h_2 a as b bs
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.leftUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (P : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P],
  (CategoryTheory.Limits.prod.leftUnitor P).inv =
    CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from P) (CategoryTheory.CategoryStruct.id P)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {app : (a : B) → η.app a ⟶ θ.app a}
  {naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.Modification.naturality._autoParam}
  {app_1 : (a : B) → η.app a ⟶ θ.app a}
  {naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Oplax.OplaxTrans.Modification.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsMultiplicativeTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.trivialFibrations C).IsMultiplicative
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.of_span_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {s : Set S},
  Ideal.span s = ⊤ → (∀ x ∈ s, Algebra.IsLocalIso R (Localization.Away x)) → Algebra.IsLocalIso R S
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKeyD.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → α → α → Prop),
  (∀ (fallback : α), motive Std.DTreeMap.Internal.Impl.leaf fallback fallback) →
    (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (x : α),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x k) →
      (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
          (fallback : α),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) fallback
              ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKeyD fallback) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              fallback ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKeyD fallback)) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β) (a_1 : α), motive a a_1 (a.minKeyD a_1)
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.runModInitCore : String → IO Bool
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.ordered : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {l : Std.DTreeMap.Internal.Impl α β}, l.WF → l.Ordered
-- Mathlib.Analysis.Complex.Norm
Complex.dist_conj_self : ∀ (z : ℂ), dist ((starRingEnd ℂ) z) z = 2 * |z.im|
-- Mathlib.Algebra.Group.Fin.Basic
Fin.neg_natCast_eq_one : ∀ (n : ℕ), -↑n = 1