mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.Ord
Std.TransCmp.isGE_trans : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  (cmp a b).isGE = true → (cmp b c).isGE = true → (cmp a c).isGE = true
-- Mathlib.Tactic.FunProp.Types
/-- Default names to unfold  -/
Mathlib.Meta.FunProp.defaultUnfoldPred : Lean.Name → Bool
-- Lean.Util.PPExt
Lean.formatRawTerm : Lean.PPContext → Lean.Term → Std.Format
-- Mathlib.CategoryTheory.Category.ULift
/-- The type-level equivalence between `C` and `ULiftHom C`.  -/
CategoryTheory.ULiftHom.objEquiv : {C : Type u_1} → C ≃ CategoryTheory.ULiftHom C
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_of_ac_of_integrable : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      InformationTheory.klDiv μ ν =
        ENNReal.ofReal (∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ν.real Set.univ - μ.real Set.univ)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_congr : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {f g : R →+* S} {s t : S}
  {φ ψ : Polynomial R}, f = g → s = t → φ = ψ → Polynomial.eval₂ f s φ = Polynomial.eval₂ g t ψ
-- Mathlib.Topology.Separation.Hausdorff
pairwise_disjoint_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X], Pairwise (Function.onFun Disjoint nhds)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.IsSplitMono.id_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [hf : CategoryTheory.IsSplitMono f]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) h) = h
-- Mathlib.Geometry.Manifold.BumpFunction
/-- A smooth bump function is infinitely smooth.  -/
SmoothBumpFunction.contMDiff : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M],
  ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ↑f
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.kleinFour_isKleinFour : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 → IsKleinFour ↥(alternatingGroup.kleinFour α)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.homEquiv_def : ∀ (J : Type u_1) [inst : LinearOrder J] {i j : CategoryTheory.SimplicialThickening J},
  CategoryTheory.EnrichedOrdinaryCategory.homEquiv =
    CategoryTheory.nerveEquiv.symm.trans (CategoryTheory.nerve (i ⟶ j)).unitHomEquiv.symm
-- Mathlib.Lean.Meta.Simp
/-- Returns all declarations with the `simp`-attribute `simpAttr`.
Note: this also returns many auxiliary declarations.  -/
Lean.Meta.getAllSimpDecls : Lean.Name → Lean.CoreM (List Lean.Name)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_notMem_div_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {s t : Finset α}, 1 ∉ s / t ↔ Disjoint s t
-- Mathlib.RingTheory.Ideal.UFD
Ideal.isPrincipal_of_isPrincipal_isLocalizationAway_of_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [WfDvdMonoid R] {x : R},
  Prime x →
    ∀ {p : Ideal R} [p.IsPrime],
      x ∉ p →
        ∀ (S : Type u_2) [inst_4 : CommRing S] [inst_5 : Algebra R S] [IsLocalization.Away x S],
          Submodule.IsPrincipal (Ideal.map (algebraMap R S) p) → Submodule.IsPrincipal p
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.instEncodableOfSigmaNatFunctions : {L : FirstOrder.Language} → {α : Type u'} → [Encodable α] → [Encodable ((i : ℕ) × L.Functions i)] → Encodable (L.Term α)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndepOn_id_union_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s t : Set M},
  Disjoint s t →
    (LinearIndepOn R id (s ∪ t) ↔
      LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (Submodule.span R s) (Submodule.span R t))
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.ofNat_ctorIdx : ∀ (x : CategoryTheory.Limits.WalkingReflexivePair), CategoryTheory.Limits.WalkingReflexivePair.ofNat x.ctorIdx = x
-- Std.Time.Format
/-- Formats a `DateTime` value into a simple date time with timezone string.
 -/
Std.Time.DateTime.toDateTimeWithZoneString : Std.Time.DateTime → String
-- Mathlib.Algebra.GradedMulAction
/-- Multiplication is homogeneous  -/
SetLike.GradedSMul.smul_mem : ∀ {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} {inst : SetLike S R}
  {inst_1 : SetLike N M} {inst_2 : SMul R M} {inst_3 : VAdd ιA ιB} {A : ιA → S} {B : ιB → N}
  [self : SetLike.GradedSMul A B] ⦃i : ιA⦄ ⦃j : ιB⦄ {ai : R} {bj : M}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i +ᵥ j)
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α},
  Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (toAddEquiv : E ≃+ E') (inl_comm : ⇑toAddEquiv ∘ ⇑S.inl = ⇑S'.inl)
  (rightHom_comm : ⇑S'.rightHom ∘ ⇑toAddEquiv = ⇑S.rightHom) (toAddEquiv_1 : E ≃+ E')
  (inl_comm_1 : ⇑toAddEquiv_1 ∘ ⇑S.inl = ⇑S'.inl) (rightHom_comm_1 : ⇑S'.rightHom ∘ ⇑toAddEquiv_1 = ⇑S.rightHom),
  ({ toAddEquiv := toAddEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
      { toAddEquiv := toAddEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 }) =
    (toAddEquiv = toAddEquiv_1)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.restrict_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] {V : Set X}
  (D : Function.locallyFinsuppWithin U Y) (h : V ⊆ U) (z : X), (D.restrict h) z = if z ∈ V then D z else 0
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap_self : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] (a : α),
  LinearOrderedField.cutMap α a = Set.Iio a ∩ Set.range Rat.cast
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.isPullback_χ_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type (max u v))} (m : F ⟶ G) [inst_1 : CategoryTheory.Mono m],
  CategoryTheory.IsPullback m
    ((CategoryTheory.Sheaf.isTerminalTerminal J CategoryTheory.Limits.Types.isTerminalPUnit).from F)
    (CategoryTheory.Sheaf.χ m) (CategoryTheory.Sheaf.truth J)
-- Mathlib.CategoryTheory.Action.Basic
Action.comp_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N K : Action V G}
  (f : M ⟶ N) (g : N ⟶ K), (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj_unit_app : ∀ (V : Type u_1) [inst : CategoryTheory.ReflQuiver V],
  CategoryTheory.ReflQuiv.adj.unit.app (CategoryTheory.ReflQuiv.of V) = CategoryTheory.Cat.toFreeRefl V
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- A compact set that contains `expMapBasis '' closure (paramSet K)` and furthermore is almost
equal to it, see `compactSet_ae`.
 -/
NumberField.mixedEmbedding.fundamentalCone.compactSet : (K : Type u_1) → [inst : Field K] → [NumberField K] → Set (NumberField.mixedEmbedding.realSpace K)
-- Mathlib.Tactic.Zify
/-- `zify` rewrites the main goal by shifting propositions from `ℕ` to `ℤ`.
This is often useful since `ℤ` has well-behaved subtraction.

`zify` makes use of the `@[zify_simps]` attribute to insert casts into propositions, and the
`push_cast` tactic to simplify the `ℤ`-valued expressions.

`zify` is in some sense dual to the `lift` tactic. `lift (z : Int) to Nat` will change the type of
an integer `z` (in the supertype) to `Nat` (the subtype), given a proof that `z ≥ 0`; propositions
concerning `z` will still be over `Int`. `zify` changes propositions about `Nat` (the subtype) to
propositions about `Int` (the supertype), without changing the type of any variable.

* `zify at l1 l2 ...` rewrites at the given locations.
* `zify [h₁, ..., hₙ]` uses the expressions `h₁`, ..., `hₙ` as extra lemmas for simplification.
  This is especially useful in the presence of nat subtraction or of division: passing arguments of
  type `· ≤ ·` will allow `push_cast` to do more work.

Examples:
```
example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  zify
  zify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/
  sorry

example (a b c : Nat) (h : a - b < c) (hab : b ≤ a) : False := by
  -- Nonnegativity hypothesis allows pushing `· - ·`.
  zify [hab] at h
  /- h : ↑a - ↑b < ↑c -/
  sorry
```
 -/
Mathlib.Tactic.Zify.zify : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  dist x y ≤ ε₂ - ε₁ → Metric.ball x ε₁ ⊆ Metric.ball y ε₂
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranAdjunction.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D) (H : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F],
  L.ranAdjunction H =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := fun F G => ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F).symm,
        homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιK : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C} {X₁ : A} {X₃ : C}
  (f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)) {K : A}
  (α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [inst_3 : ι.Full],
  (CategoryTheory.shiftFunctor C 1).map (ι.map (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α)) =
    CategoryTheory.CategoryStruct.comp α f₃
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.eventually_not : ∀ {α : Type u} {f : Ultrafilter α} {p : α → Prop}, (∀ᶠ (x : α) in ↑f, ¬p x) ↔ ¬∀ᶠ (x : α) in ↑f, p x
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorph_trans : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ Y) (f : Y ≃ Z) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s)
  (hf : ∀ (s : Set Z), IsOpen (⇑f ⁻¹' s) ↔ IsOpen s),
  (e.trans f).toHomeomorph ⋯ = (e.toHomeomorph he).trans (f.toHomeomorph hf)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.trans : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
  {c c' : ℝ} {f : α → E} {g : α → F} {k : α → G} {l : Filter α},
  Asymptotics.IsBigOWith c l f g → Asymptotics.IsBigOWith c' l g k → 0 ≤ c → Asymptotics.IsBigOWith (c * c') l f k
-- Mathlib.Order.Bounds.Image
Monotone.image_upperBounds_subset_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {s : Set α}, f '' upperBounds s ⊆ upperBounds (f '' s)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
_private.Mathlib.Topology.ContinuousMap.Bounded.Normed.0.zpowRec.match_1.splitter : {G : Type u_2} →
  (motive : ℤ → G → Sort u_1) →
    (x : ℤ) →
      (x_1 : G) →
        ((n : ℕ) → (a : G) → motive (Int.ofNat n) a) → ((n : ℕ) → (a : G) → motive (Int.negSucc n) a) → motive x x_1
-- Mathlib.Probability.Moments.Covariance
/-- The covariance of two real-valued random variables defined as
the integral of `(X - 𝔼[X])(Y - 𝔼[Y])`.  -/
ProbabilityTheory.covariance : {Ω : Type u_1} → {mΩ : MeasurableSpace Ω} → (Ω → ℝ) → (Ω → ℝ) → MeasureTheory.Measure Ω → ℝ
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} {f f' : E ⟶ E'},
  f = f' ↔ ∀ (r : ℤ) (hr : r₀ ≤ r), f.hom r ⋯ = f'.hom r ⋯
-- Mathlib.Order.Monotone.Defs
instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {f : α → β} → {s : Set α} → [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f b ≤ f a)] → Decidable (AntitoneOn f s)
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.init_snoc : ∀ {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ Set.range ⇑x),
  Fin.Embedding.init (Fin.Embedding.snoc x ha) = x
-- Mathlib.Topology.Order.NhdsSet
Ici_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  a < b → Set.Ici a ∈ nhdsSet (Set.Ico b c)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_comp : ∀ (f g : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp (f.comp g) k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.comp g) k) ∪
      Turing.PartrecToTM2.codeSupp g (Turing.PartrecToTM2.Cont'.comp f k)
-- Mathlib.Data.Nat.Cast.Basic
Even.natCast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] {n : ℕ}, Even n → Even ↑n
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_natCast : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ), (↑n).zmodRepr = n % p
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.partialEquivLimit.eq_1 : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N),
  FirstOrder.Language.DirectLimit.partialEquivLimit S =
    { dom := ⨆ i, (S i).dom, cod := ⨆ i, (S i).cod,
      toEquiv :=
        (FirstOrder.Language.DirectLimit.Equiv_iSup { toFun := fun i => (S i).cod, monotone' := ⋯ }).comp
          ((FirstOrder.Language.DirectLimit.equiv_lift L ι (fun i => ↥(S i).dom)
                (fun x x_1 hij => FirstOrder.Language.Substructure.inclusion ⋯) (fun i => ↥(S i).cod)
                (fun x x_1 hij => FirstOrder.Language.Substructure.inclusion ⋯) (fun i => (S i).toEquiv) ⋯).comp
            (FirstOrder.Language.DirectLimit.Equiv_iSup { toFun := fun i => (S i).dom, monotone' := ⋯ }).symm) }
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a vector and another normalized vector is equal to the angle
between the original vectors.  -/
InnerProductGeometry.angle_normalize_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x (NormedSpace.normalize y) = InnerProductGeometry.angle x y
-- Mathlib.Logic.Equiv.Set
/-- If `α` is equivalent to `β`, then `Set α` is equivalent to `Set β`.  -/
Equiv.Set.congr : {α : Type u_3} → {β : Type u_4} → α ≃ β → Set α ≃ Set β
-- Mathlib.Topology.Irreducible
/-- **Alias** of the reverse direction of `isPreirreducible_iff_closure`. -/
IsPreirreducible.closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsPreirreducible s → IsPreirreducible (closure s)
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ p * exp (v * X)` is integrable for all nonnegative `p : ℝ`.  -/
ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => |X ω| ^ p * Real.exp (v * X ω)) μ
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.opLaxMonoidalPi_η : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).OplaxMonoidal] (i : I),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Functor.pi F) i = CategoryTheory.Functor.OplaxMonoidal.η (F i)
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.addSubgroupOfClosure.congr_simp : ∀ {M : Type u_7} {R : Type u_8} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : IsAddTorsionFree R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : AddSubgroup M) {ι : Type u_9} (b b_1 : Module.Basis ι R M)
  (e_b : b = b_1) (h : A = AddSubgroup.closure (Set.range ⇑b)),
  Module.Basis.addSubgroupOfClosure A b h = Module.Basis.addSubgroupOfClosure A b_1 ⋯
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C], CategoryTheory.Limits.HasProducts C
-- Mathlib.Order.Heyting.Basic
snd_hnot : ∀ {α : Type u_2} {β : Type u_3} [inst : HNot α] [inst_1 : HNot β] (a : α × β), (￢a).2 = ￢a.2
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.mkAdmAnd : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Convex.Side
AffineSubspace.setOfPred_wSameSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.WSameSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Comparing mkNatIso with the corresponding construction one can deduce from
`functorEquiv`.  -/
CategoryTheory.Limits.CategoricalPullback.mkNatIso_eq : ∀ {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₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e₂ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (coh :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
          (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
            (CategoryTheory.CategoryStruct.comp
              (K.whiskerLeft
                (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
              (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
        CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (J.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
              (CategoryTheory.Functor.whiskerRight e₂.hom G))))
      CategoryTheory.Limits.CategoricalPullback.mkNatIso_eq._auto_1),
  CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh =
    (CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).fullyFaithfulFunctor.preimageIso
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso e₁ e₂ ⋯)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtHashMap.unitOfList l).getKeyD k' fallback = k
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Constructor for morphisms in `ModuleCat R` which takes as inputs
a morphism between the underlying objects in `AddCommGrpCat` and the compatibility
with the scalar multiplication.  -/
ModuleCat.homMk : {R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      (φ :
          (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶
            (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N) →
        (∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ) →
          (M ⟶ N)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_equiv_eq_comap_symm : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R ≃+* S) (K : Subring R),
  Subring.map (↑f) K = Subring.comap (↑f.symm) K
-- Lean.Parser.Extra
Lean.Parser.unicodeSymbol.formatter : String → String → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.regular_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.MonObj A], (CategoryTheory.Mod.regular A).X = A
-- Mathlib.RingTheory.Perfection
Perfection.liftMonoidHom_symm_apply : ∀ (p : ℕ) (M : Type u_2) [inst : CommMonoid M] [inst_1 : PerfectRing M p] (N : Type u_3) [inst_2 : CommMonoid N]
  (hmn : M →* Perfection N p), (Perfection.liftMonoidHom p M N).symm hmn = (Perfection.coeffMonoidHom N p 0).comp hmn