mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.φ_mul_q : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  RatFunc.Luroth.φ✝ E * RatFunc.Luroth.q✝ E =
    Polynomial.map (algebraMap ↥K⟮RatFunc.Luroth.generator E⟯ ↥E)
      ((RatFunc.Luroth.generator E).minpolyX ↥K⟮RatFunc.Luroth.generator E⟯)
-- Init.Data.UInt.Lemmas
UInt64.pow_zero : ∀ (x : UInt64), x ^ 0 = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α},
  k ∈ m → m.getKey? k = some k
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.stronglyMeasurable_le : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} {i j : ι},
  MeasureTheory.StronglyAdapted f u → i ≤ j → MeasureTheory.StronglyMeasurable (u i)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The injective algebra homomorphism `A / (I ⊔ J) → (A / I) / J'` induced by `quotQuotMk`,
where `J'` is the projection `J` in `A / I`.  -/
DoubleQuot.liftSupQuotQuotMkₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] → (I J : Ideal A) → A ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.exists_eq_mul_self : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] (x : k), ∃ z, x = z * z
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec3_dotProduct' : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Mul α] {a₀ a₁ a₂ b₀ b₁ b₂ : α},
  ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesRightHomology : ∀ {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] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (F.mapShortComplex.obj S₁).HasHomology]
  [inst_8 : (F.mapShortComplex.obj S₂).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂]
  [F.ReflectsIsomorphisms],
  CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α),
  (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n
-- Batteries.Recycling.RBTree.Basic
/-- `path.insert t v` inserts element `v` into the tree, assuming that `(t, path)` was the result of a
previous `zoom` operation (so either the root of `t` is equivalent to `v` or it is empty).
 -/
RBTree.RBNode.Path.insert : {α : Type u_1} → RBTree.RBNode.Path α → RBTree.RBNode α → α → RBTree.RBNode α
-- Mathlib.Logic.Equiv.Set
Equiv.image_eq_iff_eq : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s t : Set α), ⇑e '' s = ⇑e '' t ↔ s = t
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_zsmul : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (z : ℤ) (x : 𝔸),
  NormedSpace.exp (z • x) = NormedSpace.exp x ^ z
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_modify : ∀ {α : Type u} {β : Type v} {m : Std.DHashMap.Internal.Raw₀ α fun x => β} [inst : BEq α] [EquivBEq α]
  [inst_2 : Hashable α] [LawfulHashable α],
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : β → β}, Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.Const.modify m a f)
-- Mathlib.GroupTheory.Subgroup.Center
/-- The center of isomorphic additive groups are isomorphic.  -/
AddSubgroup.centerCongr : {G : Type u_1} →
  [inst : AddGroup G] →
    {H : Type u_2} → [inst_1 : AddGroup H] → G ≃+ H → ↥(AddSubgroup.center G) ≃+ ↥(AddSubgroup.center H)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃}
  (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_14 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_15 : TotalComplexShape c₁₂ c₃ c₄] [inst_16 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_17 : DecidableEq ι₁₂]
  [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄],
  (((CategoryTheory.GradedObject.mapBifunctor G ι₁₂ ι₃).obj
            (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ (c₁.π c₂ c₁₂) K₁.X K₂.X)).obj
        K₃.X).HasMap
    (c₁₂.π c₃ c₄)
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_one_left : ∀ (a : ℕ), Nat.ceilRoot 1 a = a
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_all : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {θ : L.BoundedFormula α l.succ}
  {v : α → M} {xs : Fin l → M}, θ.all.Realize v xs ↔ ∀ (a : M), θ.Realize v (Fin.snoc xs a)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.offset_le_rawEndPos : ∀ {s : String.Slice} {p : s.Pos}, p.offset ≤ s.rawEndPos
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X) {Y Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g],
  (E.pullbackCoverOfLeft f g).I₀ = E.I₀
-- Mathlib.Data.Multiset.UnionInter
Multiset.singleton_disjoint : ∀ {α : Type u_1} {l : Multiset α} {a : α}, Disjoint {a} l ↔ a ∉ l
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_zero : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n], Matrix.den 0 = 1
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, the complement of a singleton is connected.  -/
isConnected_compl_singleton_of_one_lt_rank : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ (x : E), IsConnected {x}ᶜ
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.mk_bijective_iff_eq_bot : ∀ {A : Type u_3} [inst : Ring A] (I : Ideal A) [inst_1 : I.IsTwoSided],
  Function.Bijective ⇑(Ideal.Quotient.mk I) ↔ I = ⊥
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.IsIso.comp_left_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) [CategoryTheory.IsIso f], CategoryTheory.CategoryStruct.comp f g = 0 ↔ g = 0
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating compatibility between `PatternModel` and `ToBackwardSearcher`.

We require the searcher to always match the longest match at the first position where the pattern
matches; see `IsValidRevSearchFrom`.
 -/
String.Slice.Pattern.Model.LawfulToBackwardSearcherModel : {ρ : Type} →
  (pat : ρ) →
    [String.Slice.Pattern.Model.PatternModel pat] →
      {σ : String.Slice → Type} →
        [String.Slice.Pattern.ToBackwardSearcher pat σ] →
          [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
            [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] → Prop
-- Init.SimpLemmas
or_iff_left_iff_imp : ∀ {a b : Prop}, (a ∨ b ↔ a) ↔ b → a
-- Mathlib.Analysis.Complex.AbsMax
Complex.isOpen_setOfPred_mem_nhds_and_isMaxOn_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {s : Set E},
  DifferentiableOn ℂ f s → IsOpen {z | s ∈ nhds z ∧ IsMaxOn (norm ∘ f) s z}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey? k' =
    if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then some k else none else t.getKey? k'
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil_iff_length_eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.Nil ↔ p.length = 0
-- Mathlib.Geometry.Manifold.ChartedSpace
ModelProd.ext_iff : ∀ {H : Type u} {H' : Type u_1} {x y : ModelProd H H'}, x = y ↔ x.1 = y.1 ∧ x.2 = y.2
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.instIsClosedImmersionSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.snd f g)
-- Init.Data.UInt.Lemmas
UInt64.mul_zero : ∀ {a : UInt64}, a * 0 = 0
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instInhabitedCont : Inhabited Turing.ToPartrec.Cont
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_leftUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Lean.Elab.App
/-- Erase entry for `binderName` from `namedArgs`.  -/
Lean.Elab.Term.eraseNamedArg : List Lean.Elab.Term.NamedArg → Lean.Name → List Lean.Elab.Term.NamedArg
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.ne_zero_of_mem_finMulAntidiag : ∀ {d n : ℕ} {f : Fin d → ℕ}, f ∈ d.finMulAntidiag n → ∀ (i : Fin d), f i ≠ 0
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_inv_Iic : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : CommGroup G] [IsOrderedMonoid G] [MeasurableInv G] [μ.IsInvInvariant] {c : G}
  {f : G → F}, MeasureTheory.IntegrableOn f (Set.Ici c⁻¹) μ → MeasureTheory.IntegrableOn (fun x => f x⁻¹) (Set.Iic c) μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} [inst_4 : Inhabited β] {f : β → β},
  m.WF →
    Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.modify m k f) k =
      (Option.map f (Std.DHashMap.Raw.Const.get? m k)).get!
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsCompl.isTopCompl_iff : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : IsCompl p q),
  Submodule.IsTopCompl p q ↔ Continuous ⇑(p.projection q h)
-- Mathlib.Order.Filter.Cofinite
Filter.frequently_cofinite_iff_infinite : ∀ {α : Type u_2} {p : α → Prop}, (∃ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | p x}.Infinite
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_eq_getD_back?_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α},
  t.maxD fallback = t.toArray.back?.getD fallback
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.continuous_qParam : ∀ {h : ℝ}, Continuous (Function.Periodic.qParam h)
-- Mathlib.Data.Set.Basic
Set.inter_eq_self_of_subset_right : ∀ {α : Type u} {s t : Set α}, t ⊆ s → s ∩ t = t
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.minimaxRisk_of_isEmpty' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} [Nonempty 𝓧] [IsEmpty 𝓨],
  ProbabilityTheory.minimaxRisk ℓ P = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- Rectangles form a π-system.  -/
isPiSystem_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  IsPiSystem (Set.image2 (fun x1 x2 => x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t})
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalars_assoc_assoc : ∀ {R₁ R₂ R₃ R₄ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] [inst_3 : CommRing R₄]
  (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄) {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₄)}
  (h : ((ModuleCat.extendScalars f₁₂).comp (ModuleCat.extendScalars f₂₃)).comp (ModuleCat.extendScalars f₃₄) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsComp f₁₂ f₂₃).hom (ModuleCat.extendScalars f₃₄))
        h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsComp f₂₃ f₃₄).hom)
        (CategoryTheory.CategoryStruct.comp
          ((ModuleCat.extendScalars f₁₂).associator (ModuleCat.extendScalars f₂₃) (ModuleCat.extendScalars f₃₄)).inv h))
-- Mathlib.Tactic.Set
/-- `set a := t with h` is a variant of `let a := t`. It adds the hypothesis `h : a = t` to
the local context and replaces `t` with `a` everywhere it can.

`set a := t with ← h` will add `h : t = a` instead.

`set! a := t with h` does not do any replacing.

```lean
example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
  set y := x with ← h2
  sorry
/-
x : Nat
y : Nat := x
h : y + y - y = 3
h2 : x = y
⊢ y + y - y = 3
-/
```
 -/
Mathlib.Tactic.setTactic : Lean.ParserDescr
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.topologicalRing : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α], IsTopologicalRing (UniformSpace.Completion α)
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoToHomologicalComplex_map_f : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) (i : β),
  ((HomologicalComplex.dgoToHomologicalComplex b V).map f).f i = f.f i
-- Std.Data.Internal.List.Associative
Std.Internal.List.constAlterKey_eq_alterKey : ∀ {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α] {β : Type v} {k : α} {f : Option β → Option β}
  {l : List ((_ : α) × β)}, Std.Internal.List.Const.alterKey k f l = Std.Internal.List.alterKey k f l
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.instFunLike.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G),
  GroupExtension.Section.instFunLike S = { coe := GroupExtension.Section.toFun, coe_injective := ⋯ }
-- Mathlib.MeasureTheory.Order.Group.Lattice
measurable_oneLePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α] [MeasurableSup α],
  Measurable oneLePart
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKey? k' =
        if compare k k' = Ordering.eq then if (f (t.get? k)).isSome = true then some k else none else t.getKey? k'
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_sdiff_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iic a \ Set.Iio b = Set.Icc b a
-- Mathlib.Data.PNat.Defs
Int.canLiftPNat : CanLift ℤ ℕ+ (fun x => ↑↑x) fun x => 0 < x
-- Mathlib.Tactic.Linter.UnusedTacticExtension
/-- `#allow_unused_tactic` takes as input a space-separated list of identifiers.
These identifiers are then allowed by the unused tactic linter:
even if these tactics do not modify goals, there will be no warning emitted.

Note: for this to work, these identifiers should be the `SyntaxNodeKind` of each tactic.

For instance, you can allow the `done` and `skip` tactics using
```lean
#allow_unused_tactic Lean.Parser.Tactic.done Lean.Parser.Tactic.skip
```

This change is file-local.  If you want a *persistent* change, then use the `!`-flag:
the command `#allow_unused_tactic! ids` makes the change the linter continues to ignore these
tactics also in files importing a file where this command is issued.

The command `#show_kind tac` may help to find the `SyntaxNodeKind`.
 -/
Mathlib.Linter.UnusedTactic.«command#allow_unused_tactic!___» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Chebyshev
/-- Special case of **Chebyshev's Sum Inequality** or the **Cauchy-Schwarz Inequality**: The square
of the sum is less than the size of the set times the sum of the squares.  -/
sq_sum_le_card_mul_sum_sq : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f : ι → α}, (∑ i ∈ s, f i) ^ 2 ≤ ↑s.card * ∑ i ∈ s, f i ^ 2
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift.eq_1 : ∀ {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),
  AddMonoid.Coprod.lift f g = AddMonoid.Coprod.clift (FreeAddMonoid.lift (Sum.elim ⇑f ⇑g)) ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The map on stalks induced by the unit commutes with maps from `Γ(X)` to
stalks (in `Spec Γ(X)` and in `X`).  -/
AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.StructureSheaf.toStalk
        (↑(Opposite.unop (Opposite.op (AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))))
        ((CategoryTheory.ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x))
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) =
    X.presheaf.Γgerm x
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.normSq ((starRingEnd K) z) = RCLike.normSq z
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (f : α → β → Bool), (Std.TreeMap.Raw.filter f t₁).Equiv (Std.TreeMap.Raw.filter f t₂)
-- Init.Data.Order.MinMaxOn
right_le_apply_maxOn : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α},
  f y ≤ f (maxOn f x y)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.coeff_divXPowOrder : ∀ {R : Type u_1} [inst : Semiring R] {f : PowerSeries R} {n : ℕ},
  (PowerSeries.coeff n) f.divXPowOrder = (PowerSeries.coeff (n + f.order.toNat)) f
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp_contDiffWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {t : Set E} {x : E} {n : WithTop ℕ∞} {g : F → G}
  {f : E → F}, ContDiff 𝕜 n g → ContDiffWithinAt 𝕜 n f t x → ContDiffWithinAt 𝕜 n (g ∘ f) t x
-- Mathlib.Order.Interval.Set.OrdConnected
OrderEmbedding.image_Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  (Set.range ⇑e).OrdConnected → ∀ (x y : α), ⇑e '' Set.Ico x y = Set.Ico (e x) (e y)
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.instSymmetricCategoryLocalizedMonoidal : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      [CategoryTheory.SymmetricCategory C] →
                        CategoryTheory.SymmetricCategory (CategoryTheory.LocalizedMonoidal L W ε)
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.

`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.find?`.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none`
 -/
Std.Iter.Total.find? : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.IteratorLoop α Id Id] → [Std.Iterators.Finite α Id] → Std.Iter.Total β → (β → Bool) → Option β
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.ciSup_add_ciSup : ∀ {ι : Type u} {ι' : Type w} (f : ι → Cardinal.{v}) [Nonempty ι] [Nonempty ι'],
  BddAbove (Set.range f) →
    ∀ (g : ι' → Cardinal.{v}), BddAbove (Set.range g) → (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j
-- Batteries.Data.Nat.Lemmas
Nat.ofBits_testBit : ∀ (x n : ℕ), (Nat.ofBits fun i => x.testBit ↑i) = x % 2 ^ n
-- Mathlib.Control.ULift
PLift.instLawfulMonad_mathlib : LawfulMonad PLift
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- Given an isomorphism between two 1-morphisms in `Adj B`, this is the
underlying isomorphism between the left adjoints.  -/
CategoryTheory.Bicategory.Adj.lIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} → {adj₁ adj₂ : a ⟶ b} → (adj₁ ≅ adj₂) → (adj₁.l ≅ adj₂.l)