ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁶ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>u : Set α<VAR>su : u ⊇ s<VAR>u_open : IsOpen u<VAR>μu : μ u ≤ μ s + ε / 2<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u<VAR>t0 : Set α<VAR>r0 : α → ℝ<VAR>t0_count : t0.Countable<VAR>t0s : t0 ⊆ s<VAR>hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)<VAR>μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0<VAR>t0_disj : t0.PairwiseDisjoint fun x => closedBall x (r0 x)<VAR>s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)<VAR>s's : s' ⊆ s<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>H : IsEmpty (SatelliteConfig α N τ)<VAR>v : Set α<VAR>s'v : v ⊇ s'<VAR>v_open : IsOpen v<VAR>μv : μ v ≤ μ s' + ε / 2 / ↑N<VAR>r1 : α → ℝ<VAR>hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v<VAR>q : BallPackage (↑s') α := { c := fun x => ↑x, r := fun x => r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>S : Fin N → Set ↑s'<VAR>S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)<VAR>hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, closedBall x (r x) ∧ ∑' (x : ↑t), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε
<VAR>α : Type u_1<VAR>inst✝⁶ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>u : Set α<VAR>su : u ⊇ s<VAR>u_open : IsOpen u<VAR>μu : μ u ≤ μ s + ε / 2<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u<VAR>t0 : Set α<VAR>r0 : α → ℝ<VAR>t0_count : t0.Countable<VAR>t0s : t0 ⊆ s<VAR>hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)<VAR>μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0<VAR>t0_disj : t0.PairwiseDisjoint fun x => closedBall x (r0 x)<VAR>s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)<VAR>s's : s' ⊆ s<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>H : IsEmpty (SatelliteConfig α N τ)<VAR>v : Set α<VAR>s'v : v ⊇ s'<VAR>v_open : IsOpen v<VAR>μv : μ v ≤ μ s' + ε / 2 / ↑N<VAR>r1 : α → ℝ<VAR>hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v<VAR>q : BallPackage (↑s') α := { c := fun x => ↑x, r := fun x => r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>S : Fin N → Set ↑s'<VAR>S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)<VAR>hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)<VAR>S_count : ∀ (i : Fin N), (S i).Countable<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, closedBall x (r x) ∧ ∑' (x : ↑t), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε
<VAR>α : Type u_1<VAR>inst✝⁶ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>u : Set α<VAR>su : u ⊇ s<VAR>u_open : IsOpen u<VAR>μu : μ u ≤ μ s + ε / 2<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u<VAR>t0 : Set α<VAR>r0 : α → ℝ<VAR>t0_count : t0.Countable<VAR>t0s : t0 ⊆ s<VAR>hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)<VAR>μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0<VAR>t0_disj : t0.PairwiseDisjoint fun x => closedBall x (r0 x)<VAR>s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)<VAR>s's : s' ⊆ s<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>H : IsEmpty (SatelliteConfig α N τ)<VAR>v : Set α<VAR>s'v : v ⊇ s'<VAR>v_open : IsOpen v<VAR>μv : μ v ≤ μ s' + ε / 2 / ↑N<VAR>r1 : α → ℝ<VAR>hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v<VAR>q : BallPackage (↑s') α := { c := fun x => ↑x, r := fun x => r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>S : Fin N → Set ↑s'<VAR>S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)<VAR>hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)<VAR>S_count : ∀ (i : Fin N), (S i).Countable<VAR>r : α → ℝ := fun x => if x ∈ s' then r1 x else r0 x<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, closedBall x (r x) ∧ ∑' (x : ↑t), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε
<VAR>α : Type u_1<VAR>inst✝⁶ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.OuterRegular<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>u : Set α<VAR>su : u ⊇ s<VAR>u_open : IsOpen u<VAR>μu : μ u ≤ μ s + ε / 2<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u<VAR>t0 : Set α<VAR>r0 : α → ℝ<VAR>t0_count : t0.Countable<VAR>t0s : t0 ⊆ s<VAR>hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)<VAR>μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0<VAR>t0_disj : t0.PairwiseDisjoint fun x => closedBall x (r0 x)<VAR>s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)<VAR>s's : s' ⊆ s<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>H : IsEmpty (SatelliteConfig α N τ)<VAR>v : Set α<VAR>s'v : v ⊇ s'<VAR>v_open : IsOpen v<VAR>μv : μ v ≤ μ s' + ε / 2 / ↑N<VAR>r1 : α → ℝ<VAR>hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v<VAR>q : BallPackage (↑s') α := { c := fun x => ↑x, r := fun x => r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>S : Fin N → Set ↑s'<VAR>S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)<VAR>hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)<VAR>S_count : ∀ (i : Fin N), (S i).Countable<VAR>r : α → ℝ := fun x => if x ∈ s' then r1 x else r0 x<VAR>r_t0 : ∀ x ∈ t0, r x = r0 x<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, closedBall x (r x) ∧ ∑' (x : ↑t), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>inst✝¹ : HasZeroMorphisms E<VAR>F₁ F₂ : C ⥤ D<VAR>inst✝ : F₁.PreservesZeroMorphisms<VAR>e : F₁ ≅ F₂<VAR>X Y : C<GOAL>F₂.map 0 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = adjoint B ↔ ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜<GOAL>A = adjoint B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>ι : Type u_5<VAR>b : Basis ι 𝕜 F<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜<VAR>x : E<GOAL>A x = (adjoint B) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Algebra A B<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>S' : Type u_7<VAR>inst✝¹ : Semiring S'<VAR>inst✝ : Algebra R S'<VAR>pb : PowerBasis R S<VAR>f g : S →ₐ[R] S'<VAR>h : f pb.gen = g pb.gen<VAR>x : S<GOAL>f x = g x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Algebra A B<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>S' : Type u_7<VAR>inst✝¹ : Semiring S'<VAR>inst✝ : Algebra R S'<VAR>pb : PowerBasis R S<VAR>f✝ g : S →ₐ[R] S'<VAR>h : f✝ pb.gen = g pb.gen<VAR>f : R[X]<GOAL>f✝ ((aeval pb.gen) f) = g ((aeval pb.gen) f)
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) + (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
<VAR>k : ℕ<GOAL>(2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝¹ : Category.{?u.10918, u_1} E<VAR>X✝¹ Y✝¹ : C<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>hF✝ hF : F.FullyFaithful<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso (F.map f)<GOAL>IsIso f
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Type u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>hS : iUnion S = univ<VAR>t : Set β<GOAL>liftCover S f hf hS ⁻¹' t = ⋃ i, Subtype.val '' (f i ⁻¹' t)
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Type u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>hS : iUnion S = univ<VAR>t : Set β<GOAL>(iUnionLift S f hf univ ⋯ ∘ fun a => ⟨a, ⋯⟩) ⁻¹' t = ⋃ i, Subtype.val '' (f i ⁻¹' t)
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Type u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>hS : iUnion S = univ<VAR>t : Set β<GOAL>(fun a => ⟨a, ⋯⟩) ⁻¹' (inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' t)) = ⋃ i, Subtype.val '' (f i ⁻¹' t)
<VAR>z : ℂ<VAR>h : ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨ (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2<GOAL>tan z = (tan ↑z.re + tanh ↑z.im * I) / (1 - tan ↑z.re * tanh ↑z.im * I)
<VAR>z : ℂ<VAR>h : ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨ (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2<GOAL>z = ↑z.re + ↑z.im * I
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Set ι<VAR>f : Π₀ (i : ι), β i<GOAL>↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>s : Set ι<VAR>f : Π₀ (i : ι), β i<GOAL>(∀ (x : ι), ¬f x = 0 → x ∈ s) ↔ ∀ i ∉ s, f i = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>ha : IsAntichain r s<VAR>hp : s.PartiallyWellOrderedOn r<GOAL>s.Finite
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>ha : IsAntichain r s<VAR>hp : s.PartiallyWellOrderedOn r<VAR>hi : s.Infinite<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>ha : IsAntichain r s<VAR>hp : s.PartiallyWellOrderedOn r<VAR>hi : s.Infinite<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h : r ↑((Infinite.natEmbedding s hi) m) ↑((Infinite.natEmbedding s hi) n)<GOAL>False
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>q : ℕ<VAR>x y : R<VAR>h : Commute x y<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x - y) ^ q = x ^ q - y ^ q
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq V<VAR>A : Matrix V V α<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>v w : V<GOAL>⋯.toGraph.Adj v w ↔ h.toGraphᶜ.Adj v w
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝ : Finite ↑s<VAR>h : t ⊆ s<GOAL>Finite ↑t
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝ : Finite ↑s<VAR>h : t ⊆ s<GOAL>Finite ↑{x | x ∈ s ∧ x ∈ t}
<VAR>X✝ : Type u<VAR>inst✝³ : TopologicalSpace X✝<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ExtremallyDisconnected X<VAR>e : X ≃ₜ Y<VAR>U : Set Y<VAR>hU : IsOpen U<GOAL>IsOpen (closure U)
<VAR>X✝ : Type u<VAR>inst✝³ : TopologicalSpace X✝<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ExtremallyDisconnected X<VAR>e : X ≃ₜ Y<VAR>U : Set Y<VAR>hU : IsOpen U<GOAL>IsOpen (closure (⇑e.symm '' U))
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<GOAL>Associates.mk p ∈ (Associates.mk a).factors
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<GOAL>Associates.mk p ∈ ↑(factors' a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>(s.sup' H fun x => a) = a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>(s.sup' H fun x => a) ≤ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>a ≤ s.sup' H fun x => a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x✝ : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<VAR>k : ℕ<VAR>hk : ↑k ≤ N<VAR>x : E<GOAL>iteratedFDeriv 𝕜 k (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
<VAR>m n✝ n : ℕ<VAR>a : ZMod (n + 1)<VAR>h : ¬a.val ≤ n.succ / 2<GOAL>a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1
<VAR>m n✝ n : ℕ<VAR>a : ZMod (n + 1)<VAR>h : ¬a.val ≤ n.succ / 2<GOAL>¬a.valMinAbs * 2 = ↑(n + 1)
<VAR>m n✝ n : ℕ<VAR>a : ZMod (n + 1)<VAR>h : ¬a.val ≤ n.succ / 2<GOAL>2 * a.val = n + 1 → a.val ≤ n.succ / 2
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<GOAL>1 ≤ rexp x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : Preorder β<VAR>u : β → α<VAR>h : CauchySeq u<GOAL>Tendsto (Prod.map u u) atTop (𝓤 α)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : IsDomain R₁<VAR>inst✝⁵ : Algebra R₁ K<VAR>inst✝⁴ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝³ : Field K'<VAR>inst✝² : Algebra R₁ K'<VAR>inst✝¹ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>(↑I⁻¹).IsPrincipal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : IsDomain R₁<VAR>inst✝⁵ : Algebra R₁ K<VAR>inst✝⁴ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝³ : Field K'<VAR>inst✝² : Algebra R₁ K'<VAR>inst✝¹ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>∃ x, I⁻¹ = spanSingleton R₁⁰ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : IsDomain R₁<VAR>inst✝⁵ : Algebra R₁ K<VAR>inst✝⁴ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝³ : Field K'<VAR>inst✝² : Algebra R₁ K'<VAR>inst✝¹ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>I⁻¹ = spanSingleton R₁⁰ (generator ↑I)⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : IsDomain R₁<VAR>inst✝⁵ : Algebra R₁ K<VAR>inst✝⁴ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝³ : Field K'<VAR>inst✝² : Algebra R₁ K'<VAR>inst✝¹ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<VAR>hI : I * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1<GOAL>I⁻¹ = spanSingleton R₁⁰ (generator ↑I)⁻¹
<VAR>a b : ℝ<VAR>h : a ≠ 0<GOAL>ContinuousAt (fun x => a ^ x) b
<VAR>a b : ℝ<VAR>h : a ≠ 0<GOAL>ContinuousAt (fun x => (↑a ^ ↑x).re) b
<VAR>a b : ℝ<VAR>h : a ≠ 0<GOAL>ContinuousAt (fun x => ↑a ^ ↑x) b
<VAR>a b : ℝ<VAR>h : a ≠ 0<GOAL>↑a ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u_7<VAR>B : Type u_8<VAR>C : Type u_9<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A C<VAR>e : B ≃ₐ[A] C<VAR>x : B<GOAL>(trace A C) (e x) = (trace A B) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u_7<VAR>B : Type u_8<VAR>C : Type u_9<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A C<VAR>e : B ≃ₐ[A] C<VAR>x : B<GOAL>(LinearMap.trace A C) ((lmul A C) (e x)) = (LinearMap.trace A C) (e.toLinearEquiv.conj ((lmul A B) x))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing S<VAR>inst✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u_7<VAR>B : Type u_8<VAR>C : Type u_9<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A C<VAR>e : B ≃ₐ[A] C<VAR>x : B<VAR>x✝ : C<GOAL>((lmul A C) (e x)) x✝ = (e.toLinearEquiv.conj ((lmul A B) x)) x✝
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : ¬c₂.Rel i₂ (c₂.next i₂)<GOAL>c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂ = 0
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α β γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>F2 : Functor F<VAR>p2 : {α : Type u} → α → F α<VAR>s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>L1 : LawfulApplicative F<VAR>L2 : LawfulApplicative F<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<GOAL>mk = mk
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α β γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>F2 : Functor F<VAR>s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>L1 : LawfulApplicative F<VAR>L2 : LawfulApplicative F<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<GOAL>mk = mk
<VAR>F✝ : Type u → Type v<VAR>inst✝¹ : Applicative F✝<VAR>inst✝ : LawfulApplicative F✝<VAR>α β γ σ : Type u<VAR>F : Type u → Type u_1<VAR>F1 : Functor F<VAR>p1 : {α : Type u} → α → F α<VAR>s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β<VAR>sl1 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr1 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>F2 : Functor F<VAR>sl2 : {α β : Type u} → F α → (Unit → F β) → F α<VAR>sr2 : {α β : Type u} → F α → (Unit → F β) → F β<VAR>L1 : LawfulApplicative F<VAR>L2 : LawfulApplicative F<VAR>H1 : ∀ {α : Type u} (x : α), pure x = pure x<VAR>H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x<GOAL>mk = mk