mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- A structure that contains the data to uniquely define an ideal sheaf, consisting of
1. an ideal `I(U) ≤ Γ(X, U)` for every affine open `U`
2. a proof that `I(D(f)) = I(U)_f` for every affine open `U` and every section `f : Γ(X, U)`
3. a subset of `X` equal to the support.

Also see `Scheme.IdealSheafData.mkOfMemSupportIff` for a constructor with the condition on the
support being (usually) easier to prove.
 -/
AlgebraicGeometry.Scheme.IdealSheafData : AlgebraicGeometry.Scheme → Type u
-- Mathlib.Algebra.Group.Defs
/-- `a ^ 0 = 1`  -/
DivInvMonoid.zpow_zero' : ∀ {G : Type u} [self : DivInvMonoid G] (a : G), a ^ 0 = 1
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.ref : Lean.Elab.WhereFinallyView → Lean.Syntax
-- Lean.Compiler.IR.CompilerM
/-- Returns the list of IR declarations in reverse declaration order.  -/
Lean.IR.getDecls : Lean.Environment → List Lean.IR.Decl
-- Mathlib.Order.Category.Lat
Lat.Hom.ext : ∀ {X Y : Lat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.Logic.Lemmas
/-- **Alias** of the forward direction of `heq_iff_eq`. -/
HEq.eq : ∀ {α : Sort u_1} {a b : α}, a ≍ b → a = b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- In an additive monoid whose only unit is `0`, a sum is equal to `0` iff all terms are `0`.  -/
Finset.sum_eq_zero_iff : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [Subsingleton (AddUnits M)],
  ∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_hom_s₀_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀), e.hom.s₀ (e.inv.s₀ i) = i
-- Mathlib.Order.SuccPred.Basic
Set.OrdConnected.predOrder : {α : Type u_3} → [inst : PartialOrder α] → {s : Set α} → [s.OrdConnected] → [PredOrder α] → PredOrder ↑s
-- Mathlib.Analysis.Normed.Ring.Basic
List.nnnorm_prod_le : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] (l : List α), ‖l.prod‖₊ ≤ (List.map nnnorm l).prod
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Except.toBool.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((a : ε) → motive (Except.error a)) → motive x
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.act_incl : {R : Type u} →
  [inst : Rack R] →
    (x y : R) →
      Rack.PreEnvelGroupRel' R
        (((Rack.PreEnvelGroup.incl x).mul (Rack.PreEnvelGroup.incl y)).mul (Rack.PreEnvelGroup.incl x).inv)
        (Rack.PreEnvelGroup.incl (Shelf.act x y))
-- Mathlib.Combinatorics.Quiver.Subquiver
wideSubquiverHasCoeToSort : {V : Type u} → [inst : Quiver V] → CoeSort (WideSubquiver V) (Type u)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.toLin'Flip_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (A : LinearMap.BilinForm R M) (x : M), ⇑((LinearMap.BilinForm.toLinHomFlip A) x) = fun y => (A y) x
-- Mathlib.Algebra.Star.MonoidHom
/-- See Note [custom simps projection]  -/
StarMulEquiv.Simps.apply : {A : Type u_2} →
  {B : Type u_3} → [inst : Mul A] → [inst_1 : Mul B] → [inst_2 : Star A] → [inst_3 : Star B] → (A ≃⋆* B) → A → B
-- Mathlib.SetTheory.ZFC.PSet
PSet.instPreorder : Preorder PSet.{u_1}
-- Lean.Meta.Tactic.ElimInfo
/-- Extra arguments to the motive, after the targets, that are instantiated with
non-atomic expressions in the goal
 -/
Lean.Meta.ElimInfo.numComplexMotiveArgs : Lean.Meta.ElimInfo → ℕ
-- Init.Tactics
/-- `haveI` behaves like `have`, but inlines the value instead of producing a `have` term.  -/
Lean.Parser.Tactic.tacticHaveI__ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The sheafification functor, as a functor taking values in `Sheaf`.  -/
CategoryTheory.plusPlusSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [instCC : CategoryTheory.ConcreteCategory D FD] →
                  [∀ {X : C} (S : J.Cover X),
                        CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
                          (CategoryTheory.forget D)] →
                    [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                          CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
                      [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                        [∀ (X : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                          [(CategoryTheory.forget D).ReflectsIsomorphisms] →
                            CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Sheaf J D)
-- Lean.Parser.Command
/-- `assert_not_exists Foo Bar` asserts that the declarations `Foo` and `Bar` do not exist
in the current import scope. Used for dependency management.
 -/
Lean.Parser.Command.assertNotExists : Lean.Parser.Parser
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.toLinearEquiv_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), ↑(AlgEquiv.restrictScalars R f) = LinearEquiv.restrictScalars R ↑f
-- Mathlib.Algebra.Module.PID
Submodule.isSemisimple_torsionBy_of_irreducible : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  {a : R}, Irreducible a → IsSemisimpleModule R ↥(Submodule.torsionBy R M a)
-- Mathlib.Algebra.Star.MonoidHom
/-- The identity as a star monoid homomorphism.  -/
StarMonoidHom.id : (A : Type u_2) → [inst : Monoid A] → [inst_1 : Star A] → A →⋆* A
-- Mathlib.Combinatorics.Graph.Delete
Graph.induce_le_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α}, G.induce X ≤ G ↔ X ⊆ G.vertexSet
-- Mathlib.Data.Rel
SetRel.prod_subset_comm : ∀ {α : Type u_1} {s₁ s₂ : Set α} {R : SetRel α α} [R.IsSymm], s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R
-- Mathlib.Data.ENNReal.Basic
/-- Extension for the `positivity` tactic: `ENNReal.toReal`.  -/
Mathlib.Meta.Positivity.evalENNRealtoReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSeq.comp : ∀ {a b o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : ↑(Set.Iio b) → ↑(Set.Iio a)},
  Ordinal.IsFundamentalSeq f → Ordinal.IsFundamentalSeq g → Ordinal.IsFundamentalSeq (f ∘ g)
-- Lean.Environment
Lean.ConstantKind.noConfusionType : Sort v✝ → Lean.ConstantKind → Lean.ConstantKind → Sort v✝
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddMonCat.Hom.mk : {A B : AddMonCat} → (↑A →+ ↑B) → A.Hom B
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological semirings, as a
`RingHom`. Similar to `RingHom.compLeftContinuous`.  -/
RingHom.compLeftContinuousBounded : {β : Type v} →
  {γ : Type w} →
    (α : Type u_2) →
      [inst : TopologicalSpace α] →
        [inst_1 : SeminormedRing β] →
          [inst_2 : SeminormedRing γ] →
            (g : β →+* γ) →
              {C : NNReal} → LipschitzWith C ⇑g → BoundedContinuousFunction α β →+* BoundedContinuousFunction α γ
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.comp_noncommCoprod : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) {Q : Type u_4} [inst_3 : AddMonoid Q]
  (h : P →+ Q), h.comp (f.noncommCoprod g comm) = (h.comp f).noncommCoprod (h.comp g) ⋯
-- Init.Data.Order.Ord
List.instLawfulEqOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.LawfulEqOrd α], Std.LawfulEqOrd (List α)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instHasCoeffsCore : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ}, P.HasCoeffs P.Core
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.div_C : ∀ {R : Type u} {a : R} [inst : Field R] {p : Polynomial R}, p / Polynomial.C a = p * Polynomial.C a⁻¹
-- Mathlib.MeasureTheory.Measure.Map
/-- The pushforward of a measure. It is defined to be `0` if `f` is not an almost everywhere
measurable function.  -/
MeasureTheory.Measure.map : {α : Type u_4} →
  {β : Type u_5} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → (α → β) → MeasureTheory.Measure α → MeasureTheory.Measure β
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.full_preadditiveYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.preadditiveYoneda.Full
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → γ a} {k : α},
  t.WF →
    Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.map f t) = true →
      Std.DTreeMap.Internal.Impl.contains k t = true
-- Init.Data.Iterators.Combinators.Take
/-- This combinator is only useful for advanced use cases.

Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
type as `it.take n`.

**Marble diagram:**

```text
it          ---a----b---c--d-e--⊥
it.toTake   ---a----b---c--d-e--⊥
```

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it`.
 -/
Std.Iter.toTake : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.Iterators.Finite α Id] → Std.Iter β → Std.Iter β
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.final_eval : ∀ {α : Type u₁} {I : α → Type u₂} [inst : (s : α) → CategoryTheory.Category.{v₂, u₂} (I s)]
  [∀ (s : α), CategoryTheory.IsFiltered (I s)] (s : α), (CategoryTheory.Pi.eval I s).Final
-- Mathlib.Topology.Compactness.Compact
/-- If `p : Set X → Prop` is stable under restriction and union, and each point `x`
of a compact set `s` has a neighborhood `t` within `s` such that `p t`, then `p s` holds.  -/
IsCompact.induction_on : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ {p : Set X → Prop},
      p ∅ →
        (∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
          (∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)) → (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) → p s
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If a group satisfies the universal property of a free group with respect to a given type, then
it is free. Here the universal property is expressed as in `IsFreeGroup.unique_lift`.  -/
IsFreeGroup.ofUniqueLift : ∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G),
  (∀ {H : Type u} [inst_1 : Group H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a) → IsFreeGroup G
-- Lean.Meta.Tactic.Apply
/-- Try to convert an `Iff` into an `Eq` by applying `iff_of_eq`.
If successful, returns the new goal, and otherwise returns the original `MVarId`.

This may be regarded as being a special case of `Lean.MVarId.liftReflToEq`, specifically for `Iff`.
 -/
Lean.MVarId.iffOfEq : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- For a normed space `E`, according to `toWeakDual_continuous` the "identity mapping"
`StrongDual 𝕜 E → WeakDual 𝕜 E` is continuous. This definition implements it as a continuous linear
map.  -/
NormedSpace.Dual.continuousLinearMapToWeakDual : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → StrongDual 𝕜 E →L[𝕜] WeakDual 𝕜 E
-- Mathlib.ModelTheory.Definability
Set.definable_univ : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁}, A.Definable L Set.univ
-- Mathlib.Data.Set.Lattice
Set.sUnion_pair : ∀ {α : Type u_1} (s t : Set α), ⋃₀ {s, t} = s ∪ t
-- Init.System.IOError
IO.Error.protocolError.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.protocolError osCode details = IO.Error.protocolError osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- The evaluation map on multivariate polynomials is uniformly continuous
for the uniform structure induced by that on multivariate power series.  -/
MvPolynomial.toMvPowerSeries_uniformContinuous : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [IsUniformAddGroup R] [IsUniformAddGroup S]
  [IsLinearTopology S S], Continuous ⇑φ → MvPowerSeries.HasEval a → UniformContinuous ⇑(MvPolynomial.eval₂Hom φ a)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.refl_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} (P : HomotopicalAlgebra.PrepathObject Y) {X : C}
  (f : X ⟶ Y), (HomotopicalAlgebra.PrepathObject.RightHomotopy.refl P f).h = CategoryTheory.CategoryStruct.comp f P.ι
-- Lean.Meta.Tactic.Simp.LoopProtection
_private.Lean.Meta.Tactic.Simp.LoopProtection.0.Lean.Meta.Simp.ppOrigins : Array Lean.Meta.Origin → Lean.MetaM Lean.MessageData
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_unitIso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalFinOfNeZeroNat : {n : ℕ} → [NeZero n] → Lean.Meta.ReduceEval (Fin n)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.apriori_dist_iterate_fixedPoint_le : ∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] (x : α) (n : ℕ),
  dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist x (f x) * ↑K ^ n / (1 - ↑K)
-- Mathlib.Order.Max
IsMax.prodMk : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsMax a → IsMax b → IsMax (a, b)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms.
Then `LinearMap.nilRank φ b` is the smallest index
at which `LinearMap.polyCharpoly φ b` has a non-zero coefficient.

This number does not depend on the choice of `b`,
see `LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree`.  -/
LinearMap.nilRank : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup L] →
          [inst_2 : Module R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [Module.Free R M] →
                  [Module.Finite R M] → [Module.Finite R L] → [Module.Free R L] → (L →ₗ[R] Module.End R M) → ℕ
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (J : Type v) →
      (U : J → C) →
        (V : (i j : J) → i ≠ j → C) →
          (f : (i j : J) → (h : i ≠ j) → V i j h ⟶ U i) →
            autoParam (∀ (i j : J) (h : i ≠ j), CategoryTheory.Mono (f i j h))
                CategoryTheory.GlueData'.f_mono._autoParam →
              (f_hasPullback :
                  autoParam
                    (∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k),
                      CategoryTheory.Limits.HasPullback (f i j hij) (f i k hik))
                    CategoryTheory.GlueData'.f_hasPullback._autoParam) →
                (t : (i j : J) → (h : i ≠ j) → V i j h ⟶ V j i ⋯) →
                  (t' :
                      (i j k : J) →
                        (hij : i ≠ j) →
                          (hik : i ≠ k) →
                            (hjk : j ≠ k) →
                              CategoryTheory.Limits.pullback (f i j hij) (f i k hik) ⟶
                                CategoryTheory.Limits.pullback (f j k hjk) (f j i ⋯)) →
                    (∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
                        CategoryTheory.CategoryStruct.comp (t' i j k hij hik hjk)
                            (CategoryTheory.Limits.pullback.snd (f j k hjk) (f j i ⋯)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Limits.pullback.fst (f i j hij) (f i k hik)) (t i j hij)) →
                      (∀ (i j : J) (hij : i ≠ j),
                          CategoryTheory.CategoryStruct.comp (t i j hij) (t j i ⋯) =
                            CategoryTheory.CategoryStruct.id (V i j hij)) →
                        (∀ (i j k : J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
                            CategoryTheory.CategoryStruct.comp (t' i j k hij hik hjk)
                                (CategoryTheory.CategoryStruct.comp (t' j k i hjk ⋯ ⋯) (t' k i j ⋯ ⋯ hij)) =
                              CategoryTheory.CategoryStruct.id
                                (CategoryTheory.Limits.pullback (f i j hij) (f i k hik))) →
                          CategoryTheory.GlueData' C
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.succEquiv_coherence : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType)
  (f :
    ↥(IntermediateField.adjoin F
          (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
            Set.Iio (Order.succ i))) →ₐ[F]
      AlgebraicClosure E),
  ((Field.Emb.Cardinal.succEquiv i) f).1 = f.comp (Subalgebra.inclusion ⋯)
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.ForwardRuleMatches.mk.injEq : ∀
  (normMatches safeMatches unsafeMatches normMatches_1 safeMatches_1 unsafeMatches_1 :
    Lean.PHashSet Aesop.ForwardRuleMatch),
  ({ normMatches := normMatches, safeMatches := safeMatches, unsafeMatches := unsafeMatches } =
      { normMatches := normMatches_1, safeMatches := safeMatches_1, unsafeMatches := unsafeMatches_1 }) =
    (normMatches = normMatches_1 ∧ safeMatches = safeMatches_1 ∧ unsafeMatches = unsafeMatches_1)
-- Init.Data.UInt.Lemmas
UInt32.toNat_mod_uSizeSize : ∀ (n : UInt32), n.toNat % USize.size = n.toNat
-- Mathlib.Order.Hom.Basic
OrderEmbedding.le_iff_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α}, f a ≤ f b ↔ a ≤ b
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkNatTrans_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F F' : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (αₗ : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F')
  (αᵣ : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F')
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F'))
      _auto_105✝)
  (c : C), (CategoryTheory.Join.mkNatTrans αₗ αᵣ h).app (CategoryTheory.Join.left c) = αₗ.app c
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.add_le_of_nonpos_left : ∀ {α : Type u_1} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (a : α) {b : α}, b ≤ 0 → b + a ≤ a
-- Mathlib.GroupTheory.Coset.Card
QuotientGroup.fintype : {α : Type u_1} →
  [inst : Group α] → [Fintype α] → (s : Subgroup α) → [DecidableRel ⇑(QuotientGroup.leftRel s)] → Fintype (α ⧸ s)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ofLimitCone_ι : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C}
  {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J),
  (CategoryTheory.Limits.Bicone.ofLimitCone ht).ι j =
    ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opFunctor_obj : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : (HomologicalComplex V c)ᵒᵖ),
  (HomologicalComplex.opFunctor V c).obj X = (Opposite.unop X).op
-- Mathlib.Topology.Clopen
isClopen_range_sigmaMk : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {i : ι}, IsClopen (Set.range (Sigma.mk i))
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.ι_of_coproductDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C}
  [CategoryTheory.Limits.CoproductDisjoint X] [inst_2 : CategoryTheory.Limits.HasCoproduct X] (i : ι),
  CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- A cone is dually finitely generated (`DualFG`) if it is the dual of a finite set. Equivalently,
the cone can be written as the intersection of finitely many halfspace. It is also known as an
H-cone. This is the counterpart to `FG` (finitely generated) which states that the cone is the span
of a finite set, or a V-cone.  -/
PointedCone.DualFG : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsOrderedRing R] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : AddCommGroup N] → [inst_6 : Module R N] → (M →ₗ[R] N →ₗ[R] R) → PointedCone R N → Prop
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- In exponential characteristic one, the separable degree equals the degree.  -/
Polynomial.HasSeparableContraction.eq_degree : ∀ {F : Type u_1} [inst : CommSemiring F] {f : Polynomial F} (hf : Polynomial.HasSeparableContraction 1 f),
  hf.degree = f.natDegree
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Init.Data.Array.Find
Array.find?_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, ¬p a = true → Array.find? p (Array.replicate n a) = none