mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α} {fallback : Unit}, (m.insertManyIfNewUnit l).getD k fallback = ()
-- Batteries.Data.Stream
Std.Stream.takeTR.loop.eq_def : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (acc : List α) (x : ℕ),
  Std.Stream.takeTR.loop s acc x =
    match x with
    | 0 => (acc.reverse, s)
    | n.succ =>
      match Std.Stream.next? s with
      | none => (acc.reverse, s)
      | some (a, s) => Std.Stream.takeTR.loop s (a :: acc) n
-- Mathlib.Algebra.Group.Defs
NegZeroClass.toNeg : {G : Type u_2} → [self : NegZeroClass G] → Neg G
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCoeAddGrpCat : Coe AddCommGrpCat AddGrpCat
-- Mathlib.Data.Fin.Basic
Fin.inhabitedFinOneAdd : (n : ℕ) → Inhabited (Fin (1 + n))
-- Mathlib.Topology.Compactness.Compact
isCompact_accumulate : ∀ {X : Type u} [inst : TopologicalSpace X] {K : ℕ → Set X},
  (∀ (n : ℕ), IsCompact (K n)) → ∀ (n : ℕ), IsCompact (Set.accumulate K n)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instZeroAddGroupSeminorm.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupSeminorm.instZeroAddGroupSeminorm = { zero := { toFun := 0, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
-- Init.Data.UInt.Lemmas
USize.ofFin_lt_iff_lt : ∀ {a b : Fin USize.size}, USize.ofFin a < USize.ofFin b ↔ a < b
-- Mathlib.Analysis.Calculus.Deriv.Inv
/-- Eta-expanded form of `Differentiable.div` -/
Differentiable.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  Differentiable 𝕜 c → Differentiable 𝕜 d → (∀ (x : 𝕜), d x ≠ 0) → Differentiable 𝕜 fun i => c i / d i
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearMap.postcompUniformConvergenceCLM_apply : ∀ {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G] (𝔖 : Set (Set E))
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜₃ G]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F 𝔖),
  (ContinuousLinearMap.postcompUniformConvergenceCLM 𝔖 L) f = L ∘SL f
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Assumes right covariance.  -/
Right.mul_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [MulPosStrictMono α], 0 < a → 0 < b → 0 < a * b
-- Mathlib.Order.CompleteBooleanAlgebra
Prod.instCompleteDistribLattice : {α : Type u} → {β : Type v} → [CompleteDistribLattice α] → [CompleteDistribLattice β] → CompleteDistribLattice (α × β)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul_support_subset_prod : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  (s : HahnSeries.SummableFamily Γ R α) (t : HahnSeries.SummableFamily Γ' V β) (gh : Γ × Γ'),
  (Function.support fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset
-- Mathlib.Order.Bounded
Set.unbounded_le_inter_not_le : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Set.Unbounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Order.SupClosed
SupClosed.eq_1 : ∀ {α : Type u_3} [inst : SemilatticeSup α] (s : Set α), SupClosed s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ⊔ b ∈ s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg.inj : ∀ {a a_1 : Lean.Expr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg a = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg a_1 →
    a = a_1
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toNontrivial : ∀ {K : Type u_2} [self : DivisionSemiring K], Nontrivial K
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.instSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] →
                  [inst_5 : Semiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) → [GradedAlgebra 𝒜] → Semiring ↥(Submodule.baseChange S (𝒜 0))
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- **Alias** of `CategoryTheory.Adjunction.homEquiv_symm_apply`. -/
CategoryTheory.Adjunction.homEquiv_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) (Y : D) (g : X ⟶ G.obj Y),
  (adj.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)
-- Mathlib.Tactic.LinearCombination
/-- The `(norm := $tac)` syntax says to use `tac` as a normalization postprocessor for
`linear_combination`. The default normalizer is `ring1`, but you can override it with `ring_nf`
to get subgoals from `linear_combination` or with `skip` to disable normalization.
 -/
Mathlib.Tactic.LinearCombination.normStx : Lean.ParserDescr
-- Mathlib.Topology.Instances.CantorSet
preCantorSet_antitone : Antitone preCantorSet
-- Mathlib.Geometry.Convex.Cone.Basic
Convex.mem_toCone : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) {x : M},
  x ∈ Convex.toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.map.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (isLt : 0 < 2) (isLt_1 : 1 < 2)
  (x_3 : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩), CategoryTheory.ComposableArrows.Mk₁.map f ⟨0, isLt⟩ ⟨1, isLt_1⟩ x_3 = f
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {pos : Lean.Lsp.Position} {completionInfoPos : ℕ} {uri_1 : Lean.Lsp.DocumentUri}
  {pos_1 : Lean.Lsp.Position} {completionInfoPos_1 : ℕ},
  { uri := uri, pos := pos, completionInfoPos := completionInfoPos } =
      { uri := uri_1, pos := pos_1, completionInfoPos := completionInfoPos_1 } →
    uri = uri_1 ∧ pos = pos_1 ∧ completionInfoPos = completionInfoPos_1
-- Mathlib.Tactic.CrossRefAttribute
/-- `wikidataId` is the node kind of Wikidata identifiers: the letter `Q` followed by digits.  -/
Mathlib.CrossRef.wikidataIdKind : Lean.SyntaxNodeKind
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- The block matrix `A.fromBlocks 0 0 D` is diagonal if `A` and `D` are diagonal.  -/
Matrix.IsDiag.fromBlocks : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix m m α} {D : Matrix n n α},
  A.IsDiag → D.IsDiag → (Matrix.fromBlocks A 0 0 D).IsDiag
-- Lean.Meta.Basic
/-- Variant of `withLocalDecls` using `BinderInfo.default`
 -/
Lean.Meta.withLocalDeclsD : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        [Inhabited α] →
          Array (Lean.Name × (Array Lean.Expr → n Lean.Expr)) →
            (Array Lean.Expr → n α) → optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → n α
-- Init.Data.List.Find
List.findIdx?_eq_none_of_findIdx?_eq_none : ∀ {α : Type u_1} {xs : List α} {p q : α → Bool},
  (∀ x ∈ xs, p x = true → q x = true) → List.findIdx? q xs = none → List.findIdx? p xs = none
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeftObjCompIso_hom_app_app : ∀ {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] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D')
  (X : CategoryTheory.Functor D' E) (X_1 : C),
  ((F.whiskeringLeftObjCompIso G).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj (G.obj (F.obj X_1)))
-- Init.Data.BitVec.Lemmas
BitVec.toInt_inj : ∀ {n : ℕ} {x y : BitVec n}, x.toInt = y.toInt ↔ x = y
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuous.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {g : γ → α}, LowerSemicontinuous f → Continuous g → LowerSemicontinuous (f ∘ g)
-- Mathlib.Algebra.Group.Commute.Basic
Commute.inv_inv : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → Commute a⁻¹ b⁻¹
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.functor_ext : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  {F G : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D}
  (h₁ : ∀ (v : V), F.obj (CategoryTheory.Cat.FreeRefl.mk v) = G.obj (CategoryTheory.Cat.FreeRefl.mk v)),
  (∀ {v w : V} (f : v ⟶ w),
      F.map (CategoryTheory.Cat.FreeRefl.homMk f) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Cat.FreeRefl.homMk f))
            (CategoryTheory.eqToHom ⋯))) →
    F = G
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instMonoidalFunctorOppositeLightProfiniteModuleCatSheafCoherentTopologyPresheafToSheaf : (R : Type u) →
  [inst : CommRing R] →
    (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).Monoidal
-- Mathlib.Data.Set.NAry
/-- Symmetric statement to `Set.image_image2_distrib_right`.  -/
Set.image_image2_right_comm : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} {f : α → β' → γ}
  {g : β → β'} {f' : α → β → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f a (g b) = g' (f' a b)) → Set.image2 f s (g '' t) = g' '' Set.image2 f' s t
-- Mathlib.Order.Monotone.Monovary
Monotone.monovary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : LinearOrder ι], Monotone f → Monotone g → Monovary f g
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.equiv₀_symm_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T) {F G : CategoryTheory.Sheaf J AddCommGrpCat} (f : F ⟶ G)
  (x : ↑(F.obj.obj (Opposite.op T))),
  (CategoryTheory.Sheaf.H.map f 0) ((CategoryTheory.Sheaf.H.equiv₀ F hT).symm x) =
    (CategoryTheory.Sheaf.H.equiv₀ G hT).symm ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op T))) x)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅[a]? = none
-- Mathlib.Algebra.Group.Basic
mul_comm_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = a * (c / b)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The structure of two-sided continuous isomorphisms between groups.
Note that both the map and its inverse have to be continuous.  -/
ContinuousMulEquiv : (G : Type u) → [TopologicalSpace G] → (H : Type v) → [TopologicalSpace H] → [Mul G] → [Mul H] → Type (max u v)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A version of `Matrix.unitOfDetInvertible` with the inverse defeq to `A⁻¹` that is therefore
noncomputable.  -/
Matrix.nonsingInvUnit : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → IsUnit A.det → (Matrix n n α)ˣ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.coev_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f],
  CategoryTheory.ExponentiableMorphism.coev f = (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj f).unit
-- Aesop.RuleTac.Forward.Basic
Aesop.getForwardImplDetailHyps : Lean.MetaM (Array Lean.LocalDecl)
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig : Inhabited Mathlib.Tactic.AtomM.Recurse.Config
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.op_adj₂ : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H), t.op.adj₂ = t.adj₁.op
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.getAllUserLevelNames : Array Lean.Elab.DefViewElabHeader → List Lean.Name
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Extensionality lemma for morphisms from a module of the form `M₁ ⊗ (M₂ ⊗ M₃)`.  -/
ModuleCat.MonoidalCategory.tensor_ext₃ : ∀ {R : Type u} [inst : CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R}
  {f g :
    CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃) ⟶ M₄},
  (∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
      (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) =
        (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))) →
    f = g
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The universal derivation.  -/
PresheafOfModules.DifferentialsConstruction.derivation' : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      (φ' : S' ⟶ R) → (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').Derivation' φ'
-- Mathlib.NumberTheory.Padics.ValuativeRel
Padic.valuation_p_ne_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {Γ₀ : Type u_1} [inst : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation ℚ_[p] Γ₀)
  [v.Compatible], v ↑p ≠ 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Auxiliary definition for `vComp`.  -/
CategoryTheory.Lax.LaxTrans.vCompNaturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          (η : CategoryTheory.Lax.LaxTrans F G) →
            (θ : CategoryTheory.Lax.LaxTrans G H) →
              {a b : B} →
                (f : a ⟶ b) →
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a))
                      (H.map f) ⟶
                    CategoryTheory.CategoryStruct.comp (F.map f)
                      (CategoryTheory.CategoryStruct.comp (η.app b) (θ.app b))
-- Mathlib.FieldTheory.AbelRuffini
gal_X_sub_C_isSolvable : ∀ {F : Type u_1} [inst : Field F] (x : F), Group.IsSolvable (Polynomial.X - Polynomial.C x).Gal
-- Mathlib.Data.Rel
SetRel.comp_id : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β), R.comp SetRel.id = R
-- Mathlib.LinearAlgebra.Dual.Defs
Module.evalEquiv_toLinearMap : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.IsReflexive R M], ↑(Module.evalEquiv R M) = Module.Dual.eval R M
-- Init.Data.Int.Linear
Int.Internal.Linear.mul_eq_kk : ∀ (a b k₁ k₂ k : ℤ), a = k₁ → b = k₂ → (k₁ * k₂ == k) = true → a * b = k
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.unshift.eq_1 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F), q.unshift z 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm z
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_τ₃ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  (groupCohomology.mapShortComplexH2 f φ).τ₃ = groupCohomology.cochainsMap₃ f φ
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `IsAdjoinRootMonic.liftPolyₗ` lifts a linear map on polynomials to a linear map on `S`.  -/
IsAdjoinRootMonic.liftPolyₗ : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        {f : Polynomial R} →
          [inst_2 : Algebra R S] →
            IsAdjoinRootMonic S f →
              {T : Type u_1} → [inst_3 : AddCommGroup T] → [inst_4 : Module R T] → (Polynomial R →ₗ[R] T) → S →ₗ[R] T
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.Functor.mapShortComplex_map_τ₂ : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (F.mapShortComplex.map φ).τ₂ = F.map φ.τ₂
-- Init.Meta.Defs
Lean.Syntax.instBEq : BEq Lean.Syntax
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reps_one_id : ∀ (A : FixedDetMatrix (Fin 2) ℤ 1), ↑A 1 0 = 0 → 0 < ↑A 0 0 → |↑A 0 1| < |↑A 1 1| → A = 1
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasFiniteProducts C}
  {src tgt : C} {rel : CategoryTheory.Subobject (src ⨯ tgt)} {src_1 tgt_1 : C}
  {rel_1 : CategoryTheory.Subobject (src_1 ⨯ tgt_1)},
  { src := src, tgt := tgt, rel := rel } = { src := src_1, tgt := tgt_1, rel := rel_1 } →
    src = src_1 ∧ tgt = tgt_1 ∧ rel ≍ rel_1
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Filters the `recArgInfos` by those that describe an argument that's part of the recursive inductive
group `group`.

Because of nested inductives this function has the ability to change the `recArgInfo`.
Consider
```
inductive Tree where | node : List Tree → Tree
```
then when we look for arguments whose type is part of the group `Tree`, we want to also consider
the argument of type `List Tree`, even though that argument’s `RecArgInfo` refers to initially to
`List`.
 -/
Lean.Elab.Structural.argsInGroup : Lean.Elab.Structural.IndGroupInst →
  Array Lean.Expr →
    Lean.Expr → Array Lean.Elab.Structural.RecArgInfo → Lean.MetaM (Array Lean.Elab.Structural.RecArgInfo)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.fieldRange_subtype : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), s.subtype.fieldRange = s
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.ofEq_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : f = g) (i j : ι),
  (Homotopy.ofEq h).hom i j = 0 i j