mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Equiv.decidable.match_1.eq_2 : ∀ {α : Type u_1} (motive : Lists α → Lists α → Sort u_2) (l₁ : Lists' α false) (l₂ : Lists' α true)
  (h_1 : (l₁ l₂ : Lists' α false) → motive ⟨false, l₁⟩ ⟨false, l₂⟩)
  (h_2 : (l₁ : Lists' α false) → (l₂ : Lists' α true) → motive ⟨false, l₁⟩ ⟨true, l₂⟩)
  (h_3 : (l₁ : Lists' α true) → (l₂ : Lists' α false) → motive ⟨true, l₁⟩ ⟨false, l₂⟩)
  (h_4 : (l₁ l₂ : Lists' α true) → motive ⟨true, l₁⟩ ⟨true, l₂⟩),
  (match ⟨false, l₁⟩, ⟨true, l₂⟩ with
    | ⟨false, l₁⟩, ⟨false, l₂⟩ => h_1 l₁ l₂
    | ⟨false, l₁⟩, ⟨true, l₂⟩ => h_2 l₁ l₂
    | ⟨true, l₁⟩, ⟨false, l₂⟩ => h_3 l₁ l₂
    | ⟨true, l₁⟩, ⟨true, l₂⟩ => h_4 l₁ l₂) =
    h_2 l₁ l₂
-- Mathlib.Algebra.Ring.Ext
Semiring.toNonAssocSemiring_injective : ∀ {R : Type u}, Function.Injective (@Semiring.toNonAssocSemiring R)
-- Init.Data.Nat.Lemmas
Nat.eq_zero_of_dvd_of_div_eq_zero : ∀ {a b : ℕ}, a ∣ b → b / a = 0 → b = 0
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioc_of_Ioo : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Ioo (a i) (b i)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot : ∀ {X : AlgebraicGeometry.Scheme}, ⊥.ideal = ⊥
-- Mathlib.Algebra.Lie.SemiDirect
/-- The canonical projection of the semi-direct sum K ⋊⁅ψ⁆ L to G.
It is not, in general, a Lie algebra homomorphism, just a linear map.  -/
LieAlgebra.SemiDirectSum.projl : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → K ⋊⁅ψ⁆ L →ₗ[R] K
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T)
  (h :
    ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
      CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j))
  (i : E.I₀) {Z : C} (h_1 : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (E.f i) (CategoryTheory.CategoryStruct.comp (E.glueMorphisms f h) h_1) =
    CategoryTheory.CategoryStruct.comp (f i) h_1
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.to_rightInvOn' : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  {s : Set α},
  AntilipschitzWith K (s.domRestrict f) →
    ∀ {g : β → α} {t : Set β}, Set.MapsTo g t s → Set.RightInvOn g f t → LipschitzWith K (t.domRestrict g)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.nextn_stop : ∀ {s : Substring.Raw}, s.Valid → ∀ (n : ℕ), s.nextn n { byteIdx := s.bsize } = { byteIdx := s.bsize }
-- Init.Data.Int.Lemmas
Int.add_neg_cancel_left : ∀ (a b : ℤ), a + (-a + b) = b
-- Mathlib.Geometry.Manifold.HasGroupoid
StructureGroupoid.chart_mem_maximalAtlas : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H) [HasGroupoid M G] (x : M), chartAt H x ∈ StructureGroupoid.maximalAtlas M G
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.ext'_iff : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} {f g : X ⟶ Y},
  f = g ↔ CategoryTheory.MorphismProperty.Comma.Hom.hom f = CategoryTheory.MorphismProperty.Comma.Hom.hom g
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.central_scalar : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {r : R} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isValueOnlyTransitionCore : Lean.Meta.Match.Problem → (Lean.Expr → Lean.MetaM Bool) → Lean.MetaM Bool
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {c' : E →L[𝕜] 𝔸'},
  HasFDerivWithinAt c c' s x → ∀ (d : 𝔸'), HasFDerivWithinAt (fun y => c y * d) (d • c') s x
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_iff_forall_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)},
  l.isEmpty = true ↔ ∀ (a : α), Std.Internal.List.containsKey a l = false
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_coeff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x : MonoidAlgebra R M), MonoidAlgebra.ofCoeff x.coeff = x
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.exists_le_comp_of_isInducing : ∀ {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup E] [inst_1 : NormedField 𝕜₂]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜₂ F] [inst_4 : TopologicalSpace F] {𝕜 : Type u_11}
  [inst_5 : NontriviallyNormedField 𝕜] [inst_6 : Module 𝕜 E] [inst_7 : TopologicalSpace E] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_8 : RingHomIsometric σ₁₂] {p : Seminorm 𝕜 E},
  Continuous ⇑p →
    ∀ [PolynormableSpace 𝕜₂ F] {f : E →ₛₗ[σ₁₂] F}, Topology.IsInducing ⇑f → ∃ p₂, Continuous ⇑p₂ ∧ p ≤ p₂.comp f
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : ENNReal) (μ : MeasureTheory.Measure α) (G : Type u_7)
  [inst_1 : NormedAddCommGroup G] [inst_2 : PartialOrder G] [hp : Fact (1 ≤ p)],
  p ≠ ⊤ → DenseRange (MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg p μ G)
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.FunBinders.propagateExpectedType : Lean.Expr → Lean.Expr → Lean.Elab.Term.FunBinders.State → Lean.Elab.TermElabM Lean.Elab.Term.FunBinders.State
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.smul : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {α : Type u_5}
  [inst_3 : CommSemiring α] [inst_4 : PartialOrder α] [inst_5 : StarRing α] [StarOrderedRing α] [inst_7 : Algebra α R]
  [StarModule α R] [PosSMulStrictMono α R] {x : Matrix n n R}, x.PosDef → ∀ {a : α}, 0 < a → (a • x).PosDef
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Section` of an additive group extension is a right inverse to `S.rightHom`.  -/
AddGroupExtension.Section : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] → [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → AddGroupExtension N E G → Type (max u_2 u_3)
-- Mathlib.Order.Defs.PartialOrder
lt_of_le_not_ge : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.exactAt_op_iff : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) {i : ι}, K.op.ExactAt i ↔ K.ExactAt i
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_le_of_ne'`. -/
LE.le.lt_of_ne' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → a ≠ b → b < a
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.range_δ : ∀ {n : ℕ} (i : Fin (n + 2)), SSet.Subcomplex.range (SSet.stdSimplex.δ i) = SSet.stdSimplex.face {i}ᶜ
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The undirected angle at `p₂` between the line segments to `p₁` and
`p₃`. If either of those points equals `p₂`, this is π/2. Use
`open scoped EuclideanGeometry` to access the `∠ p₁ p₂ p₃`
notation.  -/
EuclideanGeometry.«term∠» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_fun_injective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Injective fun e => ⇑e
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp ((t.insertIfNew k v).minKey ⋯) k).isLE = true
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Product of two continuous homomorphisms on the same space.  -/
ContinuousMonoidHom.prod : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      [inst : Monoid A] →
        [inst_1 : Monoid B] →
          [inst_2 : Monoid C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] → [inst_5 : TopologicalSpace C] → (A →ₜ* B) → (A →ₜ* C) → A →ₜ* B × C
-- Mathlib.Algebra.CharP.Defs
NeZero.not_char_dvd : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] (k : ℕ) [h : NeZero ↑k], ¬p ∣ k
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.unbox.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_23) (fvarId_1 : Lean.FVarId)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_23),
  (Lean.Compiler.LCNF.LetValue.unbox fvarId h = Lean.Compiler.LCNF.LetValue.unbox fvarId_1 h_1) = (fvarId = fvarId_1)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the right by a continuous map, as a `ContinuousLinearMap`.  -/
ContinuousMap.compCLM : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (R : Type u_3) →
          (M : Type u_5) →
            [inst_2 : TopologicalSpace M] →
              [inst_3 : Semiring R] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : ContinuousAdd M] →
                    [inst_6 : Module R M] → [inst_7 : ContinuousConstSMul R M] → C(α, β) → C(β, M) →L[R] C(α, M)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_iInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Sort u_4} {δ : Type u_5}
  [inst_1 : CompleteLinearOrder δ] {f : ι → α → δ},
  (∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x) → UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_nonempty_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α →₀ M}, f.support.Nonempty ↔ f ≠ 0
-- Init.Data.Vector.Lemmas
Vector.any_eq_true : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.any p = true ↔ ∃ i, ∃ (x : i < n), p xs[i] = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] [inst_2 : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (↑(t.insertMany l ⋯)).getD k fallback = t.getD k fallback
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : A.Hom B)
  (i j : ι) {Z : V} (h : B.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (B.d i j) h) =
    CategoryTheory.CategoryStruct.comp (A.d i j) (CategoryTheory.CategoryStruct.comp (f.f j) h)
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeIso.eq_3 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x) (b : B)
  (f : CategoryTheory.FreeBicategory.Hom x b) (g : CategoryTheory.FreeBicategory.Hom b x_1),
  CategoryTheory.FreeBicategory.normalizeIso x_2 (f.comp g) =
    (CategoryTheory.Bicategory.associator ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x_2 }) f
          g).symm ≪≫
      CategoryTheory.Bicategory.whiskerRightIso (CategoryTheory.FreeBicategory.normalizeIso x_2 f) g ≪≫
        CategoryTheory.FreeBicategory.normalizeIso (CategoryTheory.FreeBicategory.normalizeAux x_2 f) g
-- Mathlib.Data.PEquiv
PEquiv.le_def : ∀ {α : Type u} {β : Type v} {f g : α ≃. β}, f ≤ g ↔ ∀ (a : α), ∀ b ∈ f a, b ∈ g a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.range_toProdMulOpposite : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  Set.range DoubleCentralizer.toProdMulOpposite = {lr | ∀ (x y : A), (MulOpposite.unop lr.2) x * y = x * lr.1 y}
-- Lean.Meta.Tactic.Grind.Types
/-- `inconsistent := true` if `ENode`s for `True` and `False` are in the same equivalence class.  -/
Lean.Meta.Grind.GoalState.inconsistent : Lean.Meta.Grind.GoalState → Bool
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.sub_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup N₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂}
  (f g : M →ₛₗ[σ₁₂] N₂) (x : M), (f - g) x = f x - g x
-- Lean.Parser.Term
Lean.Parser.Term.letNegOpt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.Grp.AB
instPreservesHomologyFunctorAddCommGrpCatColim : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.colim.PreservesHomology
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.mk_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A →ₗc[R] B} (h₁ : ∀ (x y : A), f (x + y) = f x + f y)
  (h₂ :
    ∀ (m : R) (x : A),
      { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x)
  (h₃ : CoalgebraStruct.counit ∘ₗ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } = CoalgebraStruct.counit)
  (h₄ :
    TensorProduct.map { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }
          { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } ∘ₗ
        CoalgebraStruct.comul =
      CoalgebraStruct.comul ∘ₗ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }),
  { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.le_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupNorm E}, p ≤ q ↔ ⇑p ≤ ⇑q
-- Lean.Elab.DefView
Lean.Elab.BodyProcessedSnapshot.toSnapshot : Lean.Elab.BodyProcessedSnapshot → Lean.Language.Snapshot
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.mapHomologyIso'_eq : ∀ {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 : CategoryTheory.ShortComplex C} (hr : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasHomology]
  [inst_6 : (S.map F).HasHomology] [inst_7 : F.PreservesRightHomologyOf S],
  S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm
-- Mathlib.FieldTheory.SeparablyGenerated
/-- Suppose `k` has characteristic `p` and `a₁,...,aₙ` is a transcendence basis of `K/k`.
Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set,
`{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced).

Then some subset of `a₁,...,aₙ₊₁` forms a transcendence basis over which `a₁,...,aₙ₊₁` are
separable.
 -/
exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow : ∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (p : ℕ),
  Nat.Prime p →
    (∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) →
      ∀ {a : ι → K} (n : ι) [ExpChar k p],
        (IsTranscendenceBasis k fun i => a ↑i) →
          ∃ i, (IsTranscendenceBasis k fun j => a ↑j) ∧ IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) (a i)
-- Init.Data.Range.Polymorphic.PRange
/-- The lower bound of the range. `lower` is not included in the range.
   -/
Std.Roi.lower : {α : Type u} → Std.Roi α → α
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.isRed.eq_2 : ∀ {α : Type u_1} (x : RBTree.RBNode α),
  (∀ (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α), x = RBTree.RBNode.node c l v r → False) →
    x.isRed = RBTree.RBColor.black
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.of_mod_eq_0 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] {a : ℤ} {c : ℕ}, ↑↑c = 0 → a % ↑c = 0 → ↑a = 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instNonemptyRealizeConstResult : Nonempty Lean.Environment.RealizeConstResult✝
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.exists_hasPrimitiveVectorWith : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {h e f : L}
  [IsDomain R] [CharZero R] [Nontrivial M] [Module.IsTorsionFree R M] [Module.Finite R M]
  [LieModule.IsTriangularizable R L M] (t : IsSl2Triple h e f), ∃ μ m, m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_rio : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  Std.Slice.size (Std.Rio.Sliceable.mkSlice xs *...hi) = min hi (Std.Slice.size xs)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If three points are not collinear, the angle between them is nonzero.  -/
EuclideanGeometry.angle_ne_zero_of_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, ¬Collinear ℝ {p₁, p₂, p₃} → EuclideanGeometry.angle p₁ p₂ p₃ ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_functor : CategoryTheory.Limits.walkingParallelPairOpEquiv.functor = CategoryTheory.Limits.walkingParallelPairOp
-- Mathlib.Data.List.Perm.Lattice
List.Perm.take_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α} (n : ℕ),
  xs.Perm ys → ys.Nodup → (List.take n xs).Perm (ys ∩ List.take n xs)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.reverseBraiding_eq : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [i : CategoryTheory.SymmetricCategory C], CategoryTheory.reverseBraiding C = i.toBraidedCategory
-- Mathlib.RingTheory.Unramified.LocalStructure
/-- Given `S` a finitely presented `R`-algebra, and `p` a prime of `S`. If `S` is smooth over `R`
at `p`, then there exists `f ∉ p` such that `R → S[1/f]` factors through some `R[X₁,...,Xₙ]`,
and that `S[1/f]` is standard etale over `R[X₁,...,Xₙ]`.  -/
Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S}
  [inst_3 : p.IsPrime] [Algebra.FinitePresentation R S] [Algebra.IsSmoothAt R p],
  ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        Algebra.IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffVectorBundle.congr_simp : ∀ (n n_1 : WithTop ℕ∞),
  n = n_1 →
    ∀ {𝕜 : 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 IB_1 : ModelWithCorners 𝕜 EB HB),
      IB = IB_1 →
        ∀ [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 = ContMDiffVectorBundle n_1 F E IB_1
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The product of two partial equivalences, as a partial equivalence on the product.  -/
PartialEquiv.prod : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → PartialEquiv α β → PartialEquiv γ δ → PartialEquiv (α × γ) (β × δ)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.instInhabitedStatus.default : Mathlib.Explode.Status
-- Mathlib.Topology.Inseparable
specializingMap_iff_stableUnderSpecialization_image_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure {x})
-- Init.Data.Nat.Div.Basic
Nat.zero_div : ∀ (b : ℕ), 0 / b = 0
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_cancel' : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r₁ r₂ : R}
  {s t : ↥S}, r₁ + ↑s -ₒ t + (r₂ -ₒ s) = r₁ + r₂ -ₒ t
-- Init.System.IO
IO.Process.SpawnArgs.mk.inj : ∀ {toStdioConfig : IO.Process.StdioConfig} {cmd : String} {args : Array String} {cwd : Option System.FilePath}
  {env : Array (String × Option String)} {inheritEnv setsid : Bool} {toStdioConfig_1 : IO.Process.StdioConfig}
  {cmd_1 : String} {args_1 : Array String} {cwd_1 : Option System.FilePath} {env_1 : Array (String × Option String)}
  {inheritEnv_1 setsid_1 : Bool},
  { toStdioConfig := toStdioConfig, cmd := cmd, args := args, cwd := cwd, env := env, inheritEnv := inheritEnv,
        setsid := setsid } =
      { toStdioConfig := toStdioConfig_1, cmd := cmd_1, args := args_1, cwd := cwd_1, env := env_1,
        inheritEnv := inheritEnv_1, setsid := setsid_1 } →
    toStdioConfig = toStdioConfig_1 ∧
      cmd = cmd_1 ∧ args = args_1 ∧ cwd = cwd_1 ∧ env = env_1 ∧ inheritEnv = inheritEnv_1 ∧ setsid = setsid_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Constructor for morphisms from `mappingCocone`.  -/
CochainComplex.mappingCocone.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {M : CochainComplex C ℤ} →
              (α : CochainComplex.HomComplex.Cochain K M 0) →
                (β : CochainComplex.HomComplex.Cocycle L M 1) →
                  CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0 →
                    (CochainComplex.mappingCocone φ ⟶ M)