mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.mk : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            {X Y : CategoryTheory.DifferentialObject S C} →
              (f : X.obj ⟶ Y.obj) →
                autoParam
                    (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) =
                      CategoryTheory.CategoryStruct.comp f Y.d)
                    CategoryTheory.DifferentialObject.Hom.comm._autoParam →
                  X.Hom Y
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.subgroupOf_normalizer_eq : ∀ {G : Type u_1} [inst : Group G] {H N : Subgroup G},
  H ≤ N → (Subgroup.normalizer ↑H).subgroupOf N = Subgroup.normalizer ↑(H.subgroupOf N)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true →
          Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter! m₂) k = Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_none_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.max? = none ↔ t.isEmpty = true)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
          CategoryTheory.AddMonObj.zero))
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    CategoryTheory.AddMonObj.zero
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `a₄` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.a₄ : {R : Type u} → WeierstrassCurve R → R
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_apply_eq_ofReal_integral : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ℝ)
  (s : Set α), (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ ∂μ)
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.reducible.sizeOf_spec : sizeOf Lean.ReducibilityStatus.reducible = 1
-- Std.Sat.AIG.CNF
/-- An initial state with no CNF clauses and an empty cache.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.empty : (aig : Std.Sat.AIG ℕ) → Std.Sat.AIG.toCNF.State✝ aig
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.commSemigroup.eq_1 : ∀ {α : Type u_2} [inst : CommSemigroup α], Set.commSemigroup = { toSemigroup := Set.semigroup, mul_comm := ⋯ }
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ioo_neg : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : LocallyFiniteOrder R]
  [Archimedean R] [Nontrivial R], Filter.Tendsto (fun n => Finset.Ioo (-↑n) ↑n) Filter.atTop Filter.atTop
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_preimage_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β},
  Set.InjOn f (f ⁻¹' s) → s ⊆ Set.range f → Nat.card ↑(f ⁻¹' s) = Nat.card ↑s
-- Init.Data.UInt.Bitwise
UInt8.toNat_and : ∀ (a b : UInt8), (a &&& b).toNat = a.toNat &&& b.toNat
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.compQuadraticMap_polarBilin : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {N' : Type u_8} [inst_5 : AddCommGroup N'] [inst_6 : Module R N']
  (f : N →ₗ[R] N') (Q : QuadraticMap R M N), (f.compQuadraticMap' Q).polarBilin = LinearMap.compr₂ Q.polarBilin f
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.mul_inv_cancel : ∀ {R : Type u_1} [inst : MonoidWithZero R] [inst_1 : Nontrivial R] [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)]
  [inst_3 : NoZeroDivisors R] (x : OreLocalization (nonZeroDivisors R) R), x ≠ 0 → x * x⁻¹ = 1
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- Adding map satisfying `P` into a cover gives another cover.  -/
AlgebraicGeometry.Scheme.Cover.add : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X Y : AlgebraicGeometry.Scheme} →
    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X →
      (f : Y ⟶ X) →
        autoParam (P f) AlgebraicGeometry.Scheme.Cover.add._auto_1 →
          AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X
-- Init.Data.List.Sublist
List.singleton_suffix_cons_append_singleton_iff : ∀ {α : Type u_1} {a b c : α} {l : List α}, [a] <:+ b :: (l ++ [c]) ↔ a = c
-- Lean.Expr
Lean.instInhabitedFVarIdMap : {α : Type} → Inhabited (Lean.FVarIdMap α)
-- Mathlib.CategoryTheory.Category.Bipointed
swap_comp_bipointedToPointedSnd : Bipointed.swap.comp bipointedToPointedSnd = bipointedToPointedFst
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The measurable equivalence `(α₁ → β₁) ≃ᵐ (α₂ → β₂)` induced by `α₁ ≃ α₂` and `β₁ ≃ᵐ β₂`.  -/
MeasurableEquiv.arrowCongr' : {α₁ : Type u_8} →
  {β₁ : Type u_9} →
    {α₂ : Type u_10} →
      {β₂ : Type u_11} →
        [inst : MeasurableSpace β₁] → [inst_1 : MeasurableSpace β₂] → α₁ ≃ α₂ → β₁ ≃ᵐ β₂ → (α₁ → β₁) ≃ᵐ (α₂ → β₂)
-- Lean.Declaration
Lean.InductiveVal.mk : Lean.ConstantVal → ℕ → ℕ → List Lean.Name → List Lean.Name → ℕ → Bool → Bool → Bool → Lean.InductiveVal
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.mk.injEq : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (toEquiv : X ≃ Y)
  (edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = ↑r * edist x y) (toEquiv_1 : X ≃ Y)
  (edist_eq'_1 : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv_1.toFun x) (toEquiv_1.toFun y) = ↑r * edist x y),
  ({ toEquiv := toEquiv, edist_eq' := edist_eq' } = { toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 }) =
    (toEquiv = toEquiv_1)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.exists_mem_of_rel_of_mem : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β},
  Multiset.Rel r s t → ∀ {a : α}, a ∈ s → ∃ b ∈ t, r a b
-- Init.Grind.ToInt
Lean.Grind.ToInt.Pow.mk : ∀ {α : Type u} [inst : HPow α ℕ α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x : α) (n : ℕ), ↑(x ^ n) = I.wrap (↑x ^ n)) → Lean.Grind.ToInt.Pow α I
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.monotone_triangEnvelope : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}, P ≤ Q → P.triangEnvelope ≤ Q.triangEnvelope
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.update_self : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι),
  f.update i (f i) = f
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.Simps.splitOnNotNumber.process : String → List String → String → List String
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opENorm_le_iff : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  {f : E →SL[σ₁₂] F} {M : ENNReal}, ‖f‖ₑ ≤ M ↔ ∀ (x : E), ‖f x‖ₑ ≤ M * ‖x‖ₑ
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIcc_eq_symmetricIoo_int : SummationFilter.symmetricIcc ℤ = SummationFilter.symmetricIoo ℤ
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.HasPointwiseRightKanExtensionAt.of_natIso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} (Y : D)
  [L.HasPointwiseRightKanExtensionAt F Y] (e₁ : L ≅ L') (e₂ : F ≅ F'), L'.HasPointwiseRightKanExtensionAt F' Y
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulintEquivOfZPowersEqTop_symm_apply_zpow : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) (k : ℤ),
  (intEquivOfZPowersEqTop g hg).symm (g ^ k) = Multiplicative.ofAdd k
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α}, m.insertMany (k :: l) = (m.insert k).insertMany l
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMapAddMonoidHom_apply : ∀ (R : Type u_3) (M : Type u_4) {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (B : LinearMap.BilinMap R M N),
  (LinearMap.BilinMap.toQuadraticMapAddMonoidHom R M) B = B.toQuadraticMap
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) (h : HomotopicalAlgebra.CofibrantBrownFactorization f), HomotopicalAlgebra.WeakEquivalence h.s
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.new : Lean.Lsp.RpcWireFormat → IO (UInt64 × Lean.Server.FileWorker.RpcSession)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_mk : ∀ (c : ℕ × ℕ) (cells : Finset (ℕ × ℕ)) (isLowerSet : IsLowerSet ↑cells),
  c ∈ { cells := cells, isLowerSet := isLowerSet } ↔ c ∈ cells
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.ofIsClopen_fiber_zero : ∀ {X : Type u_5} [inst : TopologicalSpace X] {U : Set X} [inst_1 : (x : X) → Decidable (x ∈ U)] (hU : IsClopen U),
  ⇑(LocallyConstant.ofIsClopen hU) ⁻¹' {0} = U
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (k, v) ∈ t.toArray ↔ t.getKey? k = some k ∧ t[k]? = some v
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.mk.sizeOf_spec : ∀ {V : Type u_1} {G : SimpleGraph V} {E : Type u_3} [inst : MetricSpace E] [inst_1 : SizeOf V] [inst_2 : SizeOf E]
  (p : V ↪ E) (unit_dist : ∀ {u v : V}, G.Adj u v → dist (p u) (p v) = 1),
  sizeOf { p := p, unit_dist := unit_dist } = 1 + sizeOf p
-- Aesop.Rule.Forward
Aesop.ForwardRule.instBEq : BEq Aesop.ForwardRule
-- Mathlib.Data.Finset.Max
/-- To rewrite from right to left, use `Monotone.map_finset_max'`.  -/
Finset.max'_image : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Monotone f → ∀ (s : Finset α) (h : (Finset.image f s).Nonempty), (Finset.image f s).max' h = f (s.max' ⋯)
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool} {k : α}, k ∈ Std.HashMap.filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') m[k] = true
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- To write a linear map between tangent spaces in coordinates amounts to precomposing and
postcomposing it with suitable coordinate changes. For a concrete version expressing the
change of coordinates as derivatives of extended charts,
see `inTangentCoordinates_eq_mfderiv_comp`.  -/
inTangentCoordinates_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [inst_11 : IsManifold I 1 M]
  [inst_12 : IsManifold I' 1 M'] {N : Type u_9} (f : N → M) (g : N → M') (ϕ : N → E →L[𝕜] E') {x₀ x : N},
  f x ∈ (chartAt H (f x₀)).source →
    g x ∈ (chartAt H' (g x₀)).source →
      inTangentCoordinates I I' f g ϕ x₀ x =
        (tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g x₀)) (g x) ∘SL
          ϕ x ∘SL (tangentBundleCore I M).coordChange (achart H (f x₀)) (achart H (f x)) (f x)
-- Mathlib.Topology.Constructions.SumProd
isClosedMap_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClosedMap Sum.inl
-- Mathlib.Algebra.Ring.Defs
add_one_mul : ∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [RightDistribClass α] (a b : α), (a + 1) * b = a * b + b
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (z : A → A → (CategoryTheory.CatCenter C)ˣ)
  (z_zero_zero : autoParam (z 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam)
  (assoc :
    autoParam (∀ (a b c : A), z (a + b) c * z a b = z a (b + c) * z b c) CategoryTheory.TwistShiftData.assoc._autoParam)
  (commShift :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam)
  (z_1 : A → A → (CategoryTheory.CatCenter C)ˣ)
  (z_zero_zero_1 : autoParam (z_1 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam)
  (assoc_1 :
    autoParam (∀ (a b c : A), z_1 (a + b) c * z_1 a b = z_1 a (b + c) * z_1 b c)
      CategoryTheory.TwistShiftData.assoc._autoParam)
  (commShift_1 :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z_1 a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam),
  ({ z := z, z_zero_zero := z_zero_zero, assoc := assoc, commShift := commShift } =
      { z := z_1, z_zero_zero := z_zero_zero_1, assoc := assoc_1, commShift := commShift_1 }) =
    (z = z_1)
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.mk.inj : ∀ {out : Lean.Widget.TaggedText (ℕ × ℕ)} {tagStack : List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ))} {column : ℕ}
  {out_1 : Lean.Widget.TaggedText (ℕ × ℕ)} {tagStack_1 : List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ))} {column_1 : ℕ},
  { out := out, tagStack := tagStack, column := column } =
      { out := out_1, tagStack := tagStack_1, column := column_1 } →
    out = out_1 ∧ tagStack = tagStack_1 ∧ column = column_1
-- Mathlib.Data.ZMod.QuotientGroup
AddAction.minimalPeriod_pos : ∀ {α : Type u_3} {β : Type u_4} [inst : AddGroup α] (a : α) [inst_1 : AddAction α β] (b : β)
  [Finite ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)], NeZero (Function.minimalPeriod (fun x => a +ᵥ x) b)
-- Mathlib.Algebra.Group.Basic
eq_of_add_neg_eq_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a + -b = 0 → a = b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Algebra.Torsor.Defs
/-- A `Group G` is a torsor for itself.  -/
Group.instTorsor : (G : Type u_1) → [inst : Group G] → Torsor G G
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_1.eq_2 : ∀ (motive : Option Bool → Option Bool → Sort u_1) (x : Option Bool) (h_1 : (x : Option Bool) → motive (some false) x)
  (h_2 : (x : Option Bool) → motive x (some false)) (h_3 : (x : Option Bool) → motive (some true) x)
  (h_4 : (x : Option Bool) → motive x (some true)) (h_5 : (x x_1 : Option Bool) → motive x x_1),
  (x = some false → False) →
    (match x, some false with
      | some false, x => h_1 x
      | x, some false => h_2 x
      | some true, x => h_3 x
      | x, some true => h_4 x
      | x, x_2 => h_5 x x_2) =
      h_2 x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonIdIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C), (CategoryTheory.Functor.mapMonIdIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.mk.injEq : ∀ (newConsts : Lean.VisibilityMap✝ (List Lean.AsyncConst✝))
  (replayKernel : Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment)) (dyn : Dynamic)
  (newConsts_1 : Lean.VisibilityMap✝ (List Lean.AsyncConst✝))
  (replayKernel_1 : Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment))
  (dyn_1 : Dynamic),
  ({ newConsts := newConsts, replayKernel := replayKernel, dyn := dyn } =
      { newConsts := newConsts_1, replayKernel := replayKernel_1, dyn := dyn_1 }) =
    (newConsts = newConsts_1 ∧ replayKernel = replayKernel_1 ∧ dyn = dyn_1)
-- Mathlib.Algebra.Group.Action.Defs
/-- This cannot be an instance because it can cause infinite loops whenever the `VAdd` arguments
are still metavariables.  -/
VAdd.comp.vaddCommClass' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd β α]
  [VAddCommClass β M α] (g : N → M), VAddCommClass β N α
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The unital ⋆-homomorphism/⋆-representation of `A` into the algebra of bounded operators on a Hilbert
space that is constructed from a positive linear functional `f` on a unital C⋆-algebra.

This is the unital version of `gnsNonUnitalStarAlgHom`.
 -/
PositiveLinearMap.gnsStarAlgHom : {A : Type u_2} →
  [inst : CStarAlgebra A] →
    [inst_1 : PartialOrder A] → [inst_2 : StarOrderedRing A] → (f : A →ₚ[ℂ] ℂ) → A →⋆ₐ[ℂ] f.GNS →L[ℂ] f.GNS
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.eq.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (a : List ((a : α) × β a))
  (a_1 : Std.DTreeMap.Internal.Cell α β k) (a_2 a_3 : List ((a : α) × β a)) (a_4 : Std.DTreeMap.Internal.Cell α β k)
  (a_5 : List ((a : α) × β a)),
  (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 a_2 =
      Std.DTreeMap.Internal.Impl.ExplorationStep.eq a_3 a_4 a_5) =
    (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_mul_toInt_lt_neg_two_pow_iff : ∀ {w : ℕ} {x y : BitVec w},
  x.toInt * y.toInt < -2 ^ (w - 1) ↔
    (BitVec.signExtend (w * 2) x * BitVec.signExtend (w * 2) y).slt (BitVec.signExtend (w * 2) (BitVec.intMin w)) = true
-- Mathlib.SetTheory.Ordinal.Notation
ONote.add.eq_2 : ∀ (x e : ONote) (n : ℕ+) (a : ONote), (e.oadd n a).add x = e.addAux n (a.add x)
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.smul' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (self : ModuleFilterBasis R M) {U : Set M},
  U ∈ self.sets → ∃ V ∈ nhds 0, ∃ W ∈ self.sets, V • W ⊆ U
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.lt_of_ne` -/
LE.le.ssubset_of_ne : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a ≠ b → a ⊂ b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Composition of a bounded continuous function and a continuous function.  -/
BoundedContinuousFunction.compContinuous : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        {δ : Type u_2} →
          [inst_2 : TopologicalSpace δ] → BoundedContinuousFunction α β → C(δ, α) → BoundedContinuousFunction δ β
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains_of_containsKey_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValue? k (List.filter (fun p => !l₂.contains p.fst) l₁) = none
-- Mathlib.CategoryTheory.Sites.Coverage
/-- An alternative characterization of the Grothendieck topology associated to a coverage `K`:
it is the infimum of all Grothendieck topologies whose associated coverage contains `K`.
 -/
CategoryTheory.Coverage.toGrothendieck_eq_sInf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C),
  K.toGrothendieck = sInf {J | K ≤ J.toCoverage}
-- Mathlib.Algebra.Lie.Basic
LieAlgebra.ext : ∀ {R : Type u} {L : Type v} {inst : CommRing R} {inst_1 : LieRing L} {x y : LieAlgebra R L},
  SMul.smul = SMul.smul → x = y
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasFDerivAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {f' g' : G →L[ℝ] E} {x : G},
  HasFDerivAt f f' x →
    HasFDerivAt g g' x → HasFDerivAt (fun t => inner 𝕜 (f t) (g t)) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.Realize.match_1.eq_1 : ∀ {L : FirstOrder.Language} {M : Type u_5} {α : Type u_3}
  (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) (x : ℕ) (_v : α → M) (_xs : Fin x → M)
  (h_1 : (x : ℕ) → (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs)
  (h_2 :
    (x : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
        (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs)
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin x)) →
          (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs)
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs)
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs),
  (match x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs with
    | x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs => h_1 x _v _xs
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs => h_2 x t₁ t₂ v xs
    | x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs => h_3 x l R ts v xs
    | x, f₁.imp f₂, v, xs => h_4 x f₁ f₂ v xs
    | x, f.all, v, xs => h_5 x f v xs) =
    h_1 x _v _xs
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balRight.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.black a x b with
    | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
    | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
    | l => h_3 l) =
    h_1 a x b