mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.AbelRuffini
gal_isSolvable_of_splits : ∀ {F : Type u_1} [inst : Field F] {p q : Polynomial F},
  Fact (Polynomial.map (algebraMap F q.SplittingField) p).Splits → Group.IsSolvable q.Gal → Group.IsSolvable p.Gal
-- Mathlib.Lean.Meta.Simp
/-- Simplify an expression using only a list of lemmas specified by name.  -/
Lean.Meta.simpOnlyNames : List Lean.Name → Lean.Expr → optParam Lean.Meta.Simp.Config { } → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.LinearAlgebra.Determinant
Pi.basisFun_det_apply : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (v : ι → ι → R),
  (Pi.basisFun R ι).det v = (Matrix.of v).det
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- **Alias** of the reverse direction of `eHolderNorm_ne_top`. -/
MemHolder.eHolderNorm_ne_top : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y},
  MemHolder r f → eHolderNorm r f ≠ ⊤
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Action of `iterateFrobeniusₛₗ` on the bottom field.  -/
IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [inst_4 : ExpChar K p] [inst_5 : Field F]
  [inst_6 : Algebra F K] [inst_7 : Algebra F L] [inst_8 : IsScalarTower F K L] [inst_9 : ExpChar F p] {n : ℕ}
  (hn : IsPurelyInseparable.exponent K L ≤ n) (a : K),
  (IsPurelyInseparable.iterateFrobeniusₛₗ F K L p hn) ((algebraMap K L) a) = a ^ p ^ n
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.le_TFAE : ∀ {ι : Type u_1} (I J : BoxIntegral.Box ι),
  [I ≤ J, ↑I ⊆ ↑J, Set.Icc I.lower I.upper ⊆ Set.Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
-- Init.Data.Option.Lemmas
Option.le_min : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α],
  (∀ (x y z : α), x ≤ y ⊓ z ↔ x ≤ y ∧ x ≤ z) → ∀ {a b c : Option α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
-- Mathlib.LinearAlgebra.Contraction
LinearMap.compRight.congr_simp : ∀ {R : Type u_1} (S : Type u_3) {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module S M₁] [inst_9 : Module S M₂]
  [inst_10 : SMulCommClass R S M₁] [inst_11 : SMulCommClass R S M₂] [inst_12 : LinearMap.CompatibleSMul M₁ M₂ S R]
  (f f_1 : M₁ →ₗ[R] M₂), f = f_1 → LinearMap.compRight S f = LinearMap.compRight S f_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsStableUnderCobaseChangeAnodyneExtensions : SSet.anodyneExtensions.IsStableUnderCobaseChange
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- If a net of upper hemicontinuous set-valued functions converges uniformly
(along a filter `l`) in the Hausdorff uniformity to a set-valued function `f` with
compact values, then `f` is upper hemicontinuous  -/
TendstoUniformlyOn.upperHemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {ι : Type u_3}
  {F : ι → α → Set β} {l : Filter ι} [l.NeBot] [inst_2 : UniformSpace β],
  TendstoUniformlyOn F f l s →
    (∀ (n : ι), UpperHemicontinuousOn (F n) s) → (∀ x ∈ s, IsCompact (f x)) → UpperHemicontinuousOn f s
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalate_eq_intercalateTR.go : ∀ (α : Type u_1) (sep : List α) {acc : Array α} {x : List α} (xs : List (List α)),
  List.intercalateTR.go✝ sep.toArray x xs acc = acc.toList ++ (List.intersperse sep (x :: xs)).flatten
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying type.  -/
SemiRingCat.carrier : SemiRingCat → Type u
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
DiscreteUniformity.eq_bot : ∀ {X : Type u_1} {u : UniformSpace X} [self : DiscreteUniformity X], u = ⊥
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiffWithinAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {x : E} {s : Set E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (fun x => Complex.exp (f x)) s x
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.finsetInf' : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {s : Finset ι} {hs : s.Nonempty} {t : ι → Set X},
  (∀ i ∈ s, Topology.IsLocallyConstructible (t i)) → Topology.IsLocallyConstructible (s.inf' hs t)
-- Lean.Meta.Tactic.Cases
/-- Split the goal in two subgoals: one containing the hypothesis `h : p` and another containing `h : ¬ p`.
 -/
Lean.MVarId.byCases : Lean.MVarId → Lean.Expr → optParam Lean.Name `h → Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)
-- Mathlib.Order.Fin.Basic
Fin.natAdd_injective : ∀ (m n : ℕ), Function.Injective (Fin.natAdd n)
-- Mathlib.Order.UpperLower.Closure
Set.OrdConnected.upperClosure_inter_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected → ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
-- Mathlib.MeasureTheory.Integral.Pi
/-- A version of **Fubini's theorem** in `n` variables, for a natural number `n`.  -/
MeasureTheory.integral_fin_nat_prod_volume_eq_prod : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : ℕ} {E : Fin n → Type u_3}
  [inst_1 : (i : Fin n) → MeasureTheory.MeasureSpace (E i)]
  [∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume] (f : (i : Fin n) → E i → 𝕜),
  ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) = ∏ i, ∫ (x : E i), f i x
-- Mathlib.Data.List.MinMax
List.index_of_argmax : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} [inst_1 : DecidableEq α] {l : List α} {m : α},
  m ∈ List.argmax f l → ∀ {a : α}, a ∈ l → f m ≤ f a → List.idxOf m l ≤ List.idxOf a l
-- Mathlib.Data.Set.Insert
Set.pair_subset_iff : ∀ {α : Type u_1} {s : Set α} {a b : α}, {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.mem_Icc_iff_nnnorm_le_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x : A},
  x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_zero_zero : ∀ {R : Type u_1} [inst : CommRing R] (m n : ℕ), Polynomial.resultant 0 0 m n = 0 ^ (m + n)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_of_mul_lt_of_nonneg_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [MulPosMono α],
  a * b < c → d ≤ a → 0 ≤ b → d * b < c
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {Z : AlgebraicGeometry.PresheafedSpace C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).inv
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
  CategoryTheory.inv (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U) =
    CategoryTheory.CategoryStruct.comp
      (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U)))
      (X.presheaf.map (CategoryTheory.eqToHom ⋯))
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The maximal sieve always exists.  -/
CategoryTheory.Sieve.sieveInhabited : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → Inhabited (CategoryTheory.Sieve X)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.isCycle_cycleBypass : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] {w : G.Walk v v}, w.IsCircuit → w.cycleBypass.IsCycle
-- Mathlib.Topology.MetricSpace.Bounded
/-- Closed balls are bounded  -/
Metric.isBounded_closedBall : ∀ {α : Type u} {x : α} {r : ℝ} [inst : PseudoMetricSpace α], Bornology.IsBounded (Metric.closedBall x r)
-- Mathlib.Order.Interval.Set.ProjIcc
Monotone.IccExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} (h : a ≤ b)
  {f : ↑(Set.Icc a b) → β}, Monotone f → Monotone (Set.IccExtend h f)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.List.toArrayAux.eq_2 : ∀ {α : Type u_1} (x : Array α) (a : α) (as : List α), (a :: as).toArrayAux x = as.toArrayAux (x.push a)
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- The derivative of `conj ∘ f ∘ conj` is `conj ∘ deriv f ∘ conj`.  -/
deriv_conj_conj : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜},
  deriv (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) = ⇑(starRingEnd 𝕜) ∘ deriv f ∘ ⇑(starRingEnd 𝕜)
-- Lean.Expr
Lean.Expr.constLevels! : Lean.Expr → List Lean.Level
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.prec : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ},
  Nat.Primrec' f →
    Nat.Primrec' g → Nat.Primrec' fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
-- Lean.Elab.Tactic.Grind.Basic
_private.Lean.Elab.Tactic.Grind.Basic.0.Lean.Elab.Tactic.Grind.getMainGoal.loop : List Lean.Meta.Grind.Goal → Lean.Elab.Tactic.Grind.GrindTacticM Lean.Meta.Grind.Goal
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_comp_eq_desc : ∀ {X Y Z W : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} {cond : CategoryTheory.CategoryStruct.comp f g = 0},
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelDesc cond) h = SemiNormedGrp.explicitCokernelDesc ⋯
-- Init.Data.Array.Lemmas
Array.not_all_eq_any_not : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (!xs.all p) = xs.any fun a => !p a
-- Mathlib.Order.Fin.Basic
Fin.predAbove_left_monotone : ∀ {n : ℕ} (i : Fin (n + 1)), Monotone fun p => p.predAbove i
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃)
  (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁), (f ∘ₛₗ g) x = f (g x)
-- Mathlib.Order.DirSupClosed
dirSupInaccOn_Iic : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] (a : α), DirSupInaccOn D (Set.Iic a)
-- Mathlib.Algebra.Torsor.Defs
/-- **Alias** of `AddGroup.instAddTorsor`.

---

An `AddGroup G` is a torsor for itself. -/
addGroupIsAddTorsor : (G : Type u_1) → [inst : AddGroup G] → AddTorsor G G
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {E : Type u_3} [inst_2 : EquivLike E α β]
  [OrderIsoClass E α β] (e : E) {s : Set α} [hs : s.OrdConnected], (⇑e '' s).OrdConnected
-- Mathlib.Tactic.TFAE
/-- `tfae_have i → j := t`, where the goal is `TFAE [P₁, P₂, ...]` introduces a hypothesis
`tfae_i_to_j : Pᵢ → Pⱼ` and proof `t` to the local context. Note that `i` and `j` are
natural number literals (beginning at 1) used as indices to specify the propositions
`P₁, P₂, ...` that appear in the goal.

Once sufficient hypotheses have been introduced by `tfae_have`, `tfae_finish` can be used to close
the goal.

All features of `have` are supported by `tfae_have`, including naming, matching,
destructuring, and goal creation.

* `tfae_have i ← j := t` adds a hypothesis in the reverse direction, of type `Pⱼ → Pᵢ`.
* `tfae_have i ↔ j := t` adds a hypothesis in the both directions, of type `Pᵢ ↔ Pⱼ`.
* `tfae_have hij : i → j := t` names the introduced hypothesis `hij` instead of `tfae_i_to_j`.
* `tfae_have i j | p₁ => t₁ | ...` matches on the assumption `p : Pᵢ`.
* `tfae_have ⟨hij, hji⟩ : i ↔ j := t` destructures the bi-implication into `hij : Pᵢ → Pⱼ`
  and `hji : Pⱼ → Pⱼ`.
* `tfae_have i → j := t ?a` creates a new goal for `?a`.

Examples:
```lean4
example (h : P → R) : TFAE [P, Q, R] := by
  tfae_have 1 → 3 := h
  -- The resulting context now includes `tfae_1_to_3 : P → R`.
  sorry
```

```lean4
-- An example of `tfae_have` and `tfae_finish`:
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish
```

```lean4
-- All features of `have` are supported by `tfae_have`:
example : TFAE [P, Q] := by
  -- assert `tfae_1_to_2 : P → Q`:
  tfae_have 1 → 2 := sorry

  -- assert `hpq : P → Q`:
  tfae_have hpq : 1 → 2 := sorry

  -- match on `p : P` and prove `Q` via `f p`:
  tfae_have 1 → 2
  | p => f p

  -- assert `pq : P → Q`, `qp : Q → P`:
  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry

  -- assert `h : P → Q`; `?a` is a new goal:
  tfae_have h : 1 → 2 := f ?a

  sorry
```
 -/
Mathlib.Tactic.TFAE.tfaeHave' : Lean.ParserDescr
-- Mathlib.Order.KrullDimension
Order.krullDim_le_one_iff_of_boundedOrder : ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α], Order.krullDim α ≤ 1 ↔ ∀ (x : α), x = ⊥ ∨ x = ⊤
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_le_iff_le_of_lt_aleph0 : ∀ {c d : Cardinal.{u}}, c < Cardinal.aleph0 → d < Cardinal.aleph0 → (Cardinal.toNat c ≤ Cardinal.toNat d ↔ c ≤ d)
-- Init.Data.List.BasicAux
_private.Init.Data.List.BasicAux.0.List.get.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : List α) → Fin x.length → Sort u_2) (a : α) (tail : List α)
  (isLt : 0 < (a :: tail).length)
  (h_1 : (a : α) → (tail : List α) → (isLt : 0 < (a :: tail).length) → motive (a :: tail) ⟨0, isLt⟩)
  (h_2 : (head : α) → (as : List α) → (i : ℕ) → (h : i.succ < (head :: as).length) → motive (head :: as) ⟨i.succ, h⟩),
  (match a :: tail, ⟨0, isLt⟩ with
    | a :: tail, ⟨0, isLt⟩ => h_1 a tail isLt
    | head :: as, ⟨i.succ, h⟩ => h_2 head as i h) =
    h_1 a tail isLt
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_of_subsingleton_inter_left : ∀ {α : Type u} {s t : Set α}, (s ∪ t).Subsingleton → s.Subsingleton
-- Mathlib.FieldTheory.AbelRuffini
_private.Mathlib.FieldTheory.AbelRuffini.0.induction_rad : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E →
    ∀ {n : ℕ}, n ≠ 0 → Group.IsSolvable (minpoly F (x ^ n)).Gal → Group.IsSolvable (minpoly F x).Gal
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- Like `add_mul_mul_invOf_mul_eq_one`, but with multiplication reversed.  -/
Matrix.add_mul_mul_invOf_mul_eq_one' : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
  [inst_5 : Invertible A] [inst_6 : Invertible C] [inst_7 : Invertible (⅟C + V * ⅟A * U)],
  (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V) = 1
-- Mathlib.Algebra.Group.Basic
sub_sub_self : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a - b) = b
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_mono' : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V),
  U ⊆ V → μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_neg : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, ∫ (x : ℝ) in a..b, -f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Algebra.Homology.DerivedCategory.Linear
DerivedCategory.instLinearHomotopyCategoryIntUpQh : ∀ (R : Type t) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : HasDerivedCategory C],
  CategoryTheory.Functor.Linear R DerivedCategory.Qh
-- Mathlib.Algebra.Algebra.Basic
faithfulSMul_iff_algebraMap_injective : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  FaithfulSMul R A ↔ Function.Injective ⇑(algebraMap R A)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.Tactic.FunProp.Theorems
/-- Get proof of a theorem.  -/
Mathlib.Meta.FunProp.GeneralTheorem.getProof : Mathlib.Meta.FunProp.GeneralTheorem → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] {i j : σ},
  i ≠ j →
    IsEmpty ↥(CategoryTheory.Limits.pullback (CategoryTheory.Limits.Sigma.ι g i) (CategoryTheory.Limits.Sigma.ι g j))
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.trans_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃), (h₁₂.trans h₂₃).h₁ = h₁₂.h₁ + h₂₃.h₁
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.mulRight_symm : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a : G),
  (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.homEquiv.eq_1 : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {n : ℕ} (m k : ℕ)
  (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalFactorizationRing.homEquiv S m k hn p =
    {
      toFun := fun f =>
        ⟨((Polynomial.UniversalFactorizationRing.factor₁ m k hn p).map ↑f,
            (Polynomial.UniversalFactorizationRing.factor₂ m k hn p).map ↑f),
          ⋯⟩,
      invFun := fun q =>
        Algebra.TensorProduct.lift (Algebra.ofId R S)
          (let __RingHom :=
            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                  q)).toRingHom;
          { toRingHom := __RingHom, commutes' := ⋯ })
          ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- The associator for tensor products of R-coalgebras, as a coalgebra equivalence.  -/
Coalgebra.TensorProduct.assoc : (R : Type u_5) →
  (S : Type u_6) →
    (M : Type u_7) →
      (N : Type u_8) →
        (P : Type u_9) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : AddCommMonoid P] →
                      [inst_6 : Module R M] →
                        [inst_7 : Module R N] →
                          [inst_8 : Module R P] →
                            [inst_9 : Module S M] →
                              [inst_10 : IsScalarTower R S M] →
                                [inst_11 : Coalgebra S M] →
                                  [inst_12 : Module S N] →
                                    [inst_13 : IsScalarTower R S N] →
                                      [inst_14 : Coalgebra S N] →
                                        [inst_15 : Coalgebra R P] →
                                          TensorProduct R (TensorProduct S M N) P ≃ₗc[S]
                                            TensorProduct S M (TensorProduct R N P)
-- Mathlib.Algebra.Polynomial.Module.FiniteDimensional
Module.AEval.isTorsion_of_finiteDimensional : ∀ (K : Type u_2) (M : Type u_3) {A : Type u_4} (a : A) [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module K M] [inst_6 : IsScalarTower K A M]
  [FiniteDimensional K A], Module.IsTorsion (Polynomial K) (Module.AEval K M a)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.prod_lt_prod_of_ne_nil : ∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] [MulLeftMono M]
  [MulRightStrictMono M] [MulRightMono M] {l : List ι},
  l ≠ [] → ∀ (f g : ι → M), (∀ i ∈ l, f i < g i) → (List.map f l).prod < (List.map g l).prod
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.baseChange_equation : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  {f : A →ₐ[S] B},
  Function.Injective ⇑f → ∀ (P : Fin 3 → A), (W'.baseChange B).Equation (⇑f ∘ P) ↔ (W'.baseChange A).Equation P
-- Std.Net.Addr
Std.Net.SocketAddressV4.instCoeSocketAddress : Coe Std.Net.SocketAddressV4 Std.Net.SocketAddress
-- Mathlib.LinearAlgebra.Dimension.LinearMap
/-- The rank of the composition of two maps is less than the minimum of their ranks.

See `lift_rank_comp_le` for the universe-polymorphic version.  -/
LinearMap.rank_comp_le : ∀ {K : Type u} {V : Type v} {V' V'₁ : Type v'} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [inst_5 : AddCommGroup V'₁] [inst_6 : Module K V'₁]
  (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁), (f ∘ₗ g).rank ≤ min f.rank g.rank
-- Std.Do.WP.SimpLemmas
Std.Do.WP.adaptExcept_EStateM : ∀ {ε ε' σ α : Type u_1} {x : EStateM ε σ α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))} (f : ε → ε'),
  (Std.Do.wp (EStateM.adaptExcept f x)).apply Q = (Std.Do.wp x).apply (Q.1, fun e => Q.2.1 (f e), Q.2.2)
-- Mathlib.Data.Vector3
/-- Get the `i`th element of a vector  -/
Vector3.nth : {α : Type u_1} → {n : ℕ} → Fin2 n → Vector3 α n → α