ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀<VAR>Λ : Module.Dual ℝ (ι → ℝ)<VAR>Λ₀ : ℝ<VAR>h0 : (Λ, Λ₀) ≠ 0<VAR>hsum : ∀ (x : E), Λ ((ContinuousLinearMap.pi f') x) + Λ₀ • φ' x = 0<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀<VAR>Λ₀ : ℝ<VAR>Λ : ι → ℝ<VAR>h0 : ((LinearEquiv.piRing ℝ ℝ ι ℝ).symm Λ, Λ₀) ≠ 0<VAR>hsum : ∀ (x : E), ((LinearEquiv.piRing ℝ ℝ ι ℝ).symm Λ) ((ContinuousLinearMap.pi f') x) + Λ₀ • φ' x = 0<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℤ<VAR>a : R<GOAL>(C a * T n).degree = if a = 0 then ⊥ else ↑n
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<GOAL>Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : ↥(Lp E p μ)<GOAL>dist f g = (eLpNorm (↑↑f - ↑↑g) p μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : ↥(Lp E p μ)<GOAL>(eLpNorm (↑↑(f - g)) p μ).toReal = (eLpNorm (↑↑f - ↑↑g) p μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : ↥(Lp E p μ)<GOAL>eLpNorm (↑↑(f - g)) p μ = eLpNorm (↑↑f - ↑↑g) p μ
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>χ.FactorsThrough 1 ↔ χ = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>x✝ : χ.FactorsThrough 1<VAR>w✝ : 1 ∣ n<VAR>χ₀ : DirichletCharacter R 1<VAR>hχ₀ : χ = (changeLevel w✝) χ₀<GOAL>χ = 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>P : ProjectiveResolution Y<VAR>Q : ProjectiveResolution Z<GOAL>liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n✝ n : ℕ<VAR>hn : n ≠ 0<GOAL>∅ ^ n = ∅
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : ℕ<VAR>IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)<VAR>h : i + 1 < c.boundaries.card<GOAL>(take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : ℕ<VAR>IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)<VAR>h : i + 1 < c.boundaries.card<VAR>A : i < c.blocks.length<GOAL>(take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : ℕ<VAR>IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)<VAR>h : i + 1 < c.boundaries.card<VAR>A : i < c.blocks.length<VAR>B : i < c.boundaries.card<GOAL>(take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)
<VAR>n : ℕ<VAR>c : CompositionAsSet n<VAR>i : ℕ<VAR>IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)<VAR>h : i + 1 < c.boundaries.card<VAR>A : i < c.blocks.length<VAR>B : i < c.boundaries.card<GOAL>↑(c.boundary ⟨i, B⟩) + c.blocks[i] = ↑(c.boundary ⟨i + 1, h⟩)
<VAR>x : Cardinal.{u_1}<VAR>n : ℕ<GOAL>x.toENatAux ≤ ↑n ↔ x ≤ ↑n
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a : E<GOAL>‖a⁻¹‖ = ‖a‖
<VAR>k : ℤ<VAR>a : Fin 2 → ℤ<GOAL>DifferentiableOn ℂ (eisSummand k a ∘ ↑ofComplex) {z | 0 < z.im}
<VAR>k : ℤ<VAR>a : Fin 2 → ℤ<GOAL>∀ x ∈ {z | 0 < z.im}, (eisSummand k a ∘ ↑ofComplex) x = (↑(a 0) * x + ↑(a 1)) ^ (-k)
<VAR>k : ℤ<VAR>a : Fin 2 → ℤ<VAR>z : ℍ<GOAL>(eisSummand k a ∘ ↑ofComplex) ↑z = (↑(a 0) * ↑z + ↑(a 1)) ^ (-k)
<VAR>m n : ℕ+<VAR>k l : ℕ<VAR>h : m.Coprime n<GOAL>(↑m ^ k).Coprime (↑n ^ l)
<VAR>m n : ℕ+<VAR>k l : ℕ<VAR>h : (↑m).Coprime ↑n<GOAL>(↑m ^ k).Coprime (↑n ^ l)
<VAR>m n : ℕ+<VAR>k l : ℕ<VAR>h : (↑m).Coprime ↑n<GOAL>(↑m).Coprime ↑n
<VAR>m : ℕ<GOAL>m ∈ factoredNumbers ∅ ↔ m ∈ {1}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g h : G<VAR>a : α<GOAL>a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>x : ℕ<VAR>x✝ : ∃ n, n * n = x<VAR>n : ℕ<VAR>hn : n * n = x<GOAL>x.sqrt * x.sqrt = x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>hr : Symmetric r<VAR>x : α × α<GOAL>x.swap ∈ interedges r s t ↔ x ∈ interedges r t s
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a b : α<VAR>hr : Symmetric r<VAR>x : α × α<GOAL>x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)<GOAL>Tendsto (fun n => u n / ↑n) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)<VAR>lnonneg : 0 ≤ l<GOAL>Tendsto (fun n => u n / ↑n) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)<VAR>lnonneg : 0 ≤ l<VAR>A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n<GOAL>Tendsto (fun n => u n / ↑n) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)<VAR>lnonneg : 0 ≤ l<VAR>A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n<VAR>B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n<GOAL>Tendsto (fun n => u n / ↑n) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)<VAR>lnonneg : 0 ≤ l<VAR>A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n<VAR>B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n<VAR>d : ℝ<VAR>hd : d < l<GOAL>∀ᶠ (b : ℕ) in atTop, d < u b / ↑b
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>hlim : ∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)<VAR>lnonneg : 0 ≤ l<VAR>A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n<VAR>B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n<VAR>d : ℝ<VAR>hd : d > l<GOAL>∀ᶠ (b : ℕ) in atTop, u b / ↑b < d
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>i : Fin n<GOAL>coeff i (truncateFun n 0) = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a c d : α<GOAL>|a - a| ≤ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>h : torsionBySet R M s = ⊤<VAR>x : M<GOAL>∀ ⦃a : ↑s⦄, ↑a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>h : torsionBySet R M s = ⊤<VAR>x : M<GOAL>x ∈ ⊤
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>a : M<GOAL>a ^ 1 = a
<VAR>D : GlueData<VAR>i : D.J<VAR>a : ↑(D.U i)<VAR>j : D.J<VAR>b : ↑(D.U j)<VAR>k : D.J<VAR>c : ↑(D.U k)<VAR>x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))<VAR>e₁ : (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst) x = ⟨i, a⟩.snd<VAR>e₂ : (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x) = ⟨j, b⟩.snd<VAR>y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))<VAR>e₃ : (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst) y = ⟨j, b⟩.snd<VAR>e₄ : (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst) ((D.t ⟨j, b⟩.fst ⟨k, c⟩.fst) y) = ⟨k, c⟩.snd<GOAL>D.Rel ⟨i, a⟩ ⟨k, c⟩
<VAR>D : GlueData<VAR>i : D.J<VAR>a : ↑(D.U i)<VAR>j : D.J<VAR>b : ↑(D.U j)<VAR>k : D.J<VAR>c : ↑(D.U k)<VAR>x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))<VAR>e₁ : (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst) x = ⟨i, a⟩.snd<VAR>e₂ : (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x) = ⟨j, b⟩.snd<VAR>y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))<VAR>e₃ : (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst) y = ⟨j, b⟩.snd<VAR>e₄ : (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst) ((D.t ⟨j, b⟩.fst ⟨k, c⟩.fst) y) = ⟨k, c⟩.snd<VAR>z : ↑(pullback (D.f j i) (D.f j k)) := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x, y), ⋯⟩<GOAL>D.Rel ⟨i, a⟩ ⟨k, c⟩
<VAR>D : GlueData<VAR>i : D.J<VAR>a : ↑(D.U i)<VAR>j : D.J<VAR>b : ↑(D.U j)<VAR>k : D.J<VAR>c : ↑(D.U k)<VAR>x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))<VAR>e₁ : (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst) x = ⟨i, a⟩.snd<VAR>e₂ : (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x) = ⟨j, b⟩.snd<VAR>y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))<VAR>e₃ : (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst) y = ⟨j, b⟩.snd<VAR>e₄ : (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst) ((D.t ⟨j, b⟩.fst ⟨k, c⟩.fst) y) = ⟨k, c⟩.snd<VAR>z : ↑(pullback (D.f j i) (D.f j k)) := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x, y), ⋯⟩<VAR>eq₁ : (D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z) = x<GOAL>D.Rel ⟨i, a⟩ ⟨k, c⟩
<VAR>D : GlueData<VAR>i : D.J<VAR>a : ↑(D.U i)<VAR>j : D.J<VAR>b : ↑(D.U j)<VAR>k : D.J<VAR>c : ↑(D.U k)<VAR>x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))<VAR>e₁ : (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst) x = ⟨i, a⟩.snd<VAR>e₂ : (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x) = ⟨j, b⟩.snd<VAR>y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))<VAR>e₃ : (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst) y = ⟨j, b⟩.snd<VAR>e₄ : (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst) ((D.t ⟨j, b⟩.fst ⟨k, c⟩.fst) y) = ⟨k, c⟩.snd<VAR>z : ↑(pullback (D.f j i) (D.f j k)) := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x, y), ⋯⟩<VAR>eq₁ : (D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z) = x<VAR>eq₂ : (pullback.snd (D.f j i) (D.f j k)) z = y<GOAL>D.Rel ⟨i, a⟩ ⟨k, c⟩
<VAR>D : GlueData<VAR>i : D.J<VAR>a : ↑(D.U i)<VAR>j : D.J<VAR>b : ↑(D.U j)<VAR>k : D.J<VAR>c : ↑(D.U k)<VAR>x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))<VAR>e₁ : (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst) x = ⟨i, a⟩.snd<VAR>e₂ : (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x) = ⟨j, b⟩.snd<VAR>y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))<VAR>e₃ : (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst) y = ⟨j, b⟩.snd<VAR>e₄ : (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst) ((D.t ⟨j, b⟩.fst ⟨k, c⟩.fst) y) = ⟨k, c⟩.snd<VAR>z : ↑(pullback (D.f j i) (D.f j k))<VAR>eq₁ : (D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z) = x<VAR>eq₂ : (pullback.snd (D.f j i) (D.f j k)) z = y<GOAL>∃ x, (D.f ⟨i, a⟩.fst ⟨k, c⟩.fst) x = ⟨i, a⟩.snd ∧ (D.f ⟨k, c⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨k, c⟩.fst) x) = ⟨k, c⟩.snd
<VAR>D : GlueData<VAR>i : D.J<VAR>a : ↑(D.U i)<VAR>j : D.J<VAR>b : ↑(D.U j)<VAR>k : D.J<VAR>c : ↑(D.U k)<VAR>x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))<VAR>e₁ : (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst) x = ⟨i, a⟩.snd<VAR>e₂ : (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨j, b⟩.fst) x) = ⟨j, b⟩.snd<VAR>y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))<VAR>e₃ : (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst) y = ⟨j, b⟩.snd<VAR>e₄ : (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst) ((D.t ⟨j, b⟩.fst ⟨k, c⟩.fst) y) = ⟨k, c⟩.snd<VAR>z : ↑(pullback (D.f j i) (D.f j k))<VAR>eq₁ : (D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z) = x<VAR>eq₂ : (pullback.snd (D.f j i) (D.f j k)) z = y<GOAL>(D.f ⟨i, a⟩.fst ⟨k, c⟩.fst) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z)) = ⟨i, a⟩.snd ∧ (D.f ⟨k, c⟩.fst ⟨i, a⟩.fst) ((D.t ⟨i, a⟩.fst ⟨k, c⟩.fst) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z))) = ⟨k, c⟩.snd
<VAR>D : GlueData<VAR>i j k : D.J<VAR>z : ↑(pullback (D.f j i) (D.f j k))<VAR>e₂ : (D.f j i) ((D.t i j) ((D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z))) = (D.f j k) ((pullback.snd (D.f j i) (D.f j k)) z)<GOAL>(D.f i k) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z)) = (D.f i j) ((D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z)) ∧ (D.f k i) ((D.t i k) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z))) = (D.f k j) ((D.t j k) ((pullback.snd (D.f j i) (D.f j k)) z))
<VAR>D : GlueData<VAR>i j k : D.J<VAR>z : ↑(pullback (D.f j i) (D.f j k))<VAR>e₂ : (D.f j i) ((D.t i j) ((D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z))) = (D.f j k) ((pullback.snd (D.f j i) (D.f j k)) z)<VAR>h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j<GOAL>(D.f i k) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z)) = (D.f i j) ((D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z)) ∧ (D.f k i) ((D.t i k) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z))) = (D.f k j) ((D.t j k) ((pullback.snd (D.f j i) (D.f j k)) z))
<VAR>D : GlueData<VAR>i j k : D.J<VAR>z : ↑(pullback (D.f j i) (D.f j k))<VAR>e₂ : (D.f j i) ((D.t i j) ((D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z))) = (D.f j k) ((pullback.snd (D.f j i) (D.f j k)) z)<VAR>h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j<VAR>h₂ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.t i k ≫ D.f k i = pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j<GOAL>(D.f i k) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z)) = (D.f i j) ((D.t j i) ((pullback.fst (D.f j i) (D.f j k)) z)) ∧ (D.f k i) ((D.t i k) ((pullback.fst (D.f i k) (D.f i j)) ((D.t' j i k) z))) = (D.f k j) ((D.t j k) ((pullback.snd (D.f j i) (D.f j k)) z))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s₁ : AffineSubspace k P<VAR>v₁₂ v₂₃ : V<GOAL>map (↑(constVAdd k P v₂₃)) (map (↑(constVAdd k P v₁₂)) s₁) = map (↑(constVAdd k P (v₂₃ + v₁₂))) s₁
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>e' : β → γ<VAR>b : β<VAR>hb : ¬∃ a, f a = b<GOAL>extend f g e' b = e' b
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α✝<VAR>a : α✝<VAR>g f✝ : α✝ → M<VAR>α : Type u_3<VAR>inst✝ : CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>(∏ k ∈ range m, f k) / ∏ k ∈ range n, f k = ∏ k ∈ filter (fun k => n ≤ k) (range m), f k
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α✝<VAR>a : α✝<VAR>g f✝ : α✝ → M<VAR>α : Type u_3<VAR>inst✝ : CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>∏ k ∈ Ico n m, f k = ∏ k ∈ filter (fun k => n ≤ k) (range m), f k
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α✝<VAR>a : α✝<VAR>g f✝ : α✝ → M<VAR>α : Type u_3<VAR>inst✝ : CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>Ico n m = filter (fun k => n ≤ k) (range m)
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α✝<VAR>a : α✝<VAR>g f✝ : α✝ → M<VAR>α : Type u_3<VAR>inst✝ : CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ filter (fun k => n ≤ k) (range m)
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α✝<VAR>a : α✝<VAR>g f✝ : α✝ → M<VAR>α : Type u_3<VAR>inst✝ : CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<GOAL>range b.toDual = ⊤
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : Dual R M<GOAL>f ∈ range b.toDual
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : Dual R M<VAR>lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)<GOAL>f ∈ range b.toDual
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : Dual R M<VAR>lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)<VAR>i : ι<GOAL>(b.toDual ((Finsupp.total ι M R ⇑b) lin_comb)) (b i) = f (b i)
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : Dual R M<VAR>lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f (b i)<VAR>i : ι<GOAL>lin_comb i = f (b i)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>inst✝ : S.HasLeftHomology<GOAL>h.cyclesIso.inv ≫ S.iCycles = h.i
<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✝⁴ : HasZeroObject C<VAR>inst✝³ : HasZeroObject D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<GOAL>0 ≫ 0 = 𝟙 (F.obj 0)
<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✝⁴ : HasZeroObject C<VAR>inst✝³ : HasZeroObject D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<GOAL>0 ≫ 0 = 𝟙 0
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>h : fract v ≠ 0<GOAL>(of v).s.get? 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>h : fract v ≠ 0<GOAL>(match some (IntFractPair.of (IntFractPair.of v).fr⁻¹), some ∘ fun p => { a := 1, b := ↑p.b } with | none, x => none | some a, f => f a) = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ K₂.carrier<GOAL>↑(index (↑K₁) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₂) U) / ↑(index (↑K₀) U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ K₂.carrier<GOAL>↑(index (↑K₁) U) ≤ ↑(index (↑K₂) U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : (interior U).Nonempty<VAR>K₁ K₂ : Compacts G<VAR>h : ↑K₁ ⊆ K₂.carrier<GOAL>0 < ↑(index (↑K₀) U)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type (max u_2 u_3)<VAR>f : ι → Ordinal.{max u_2 u_3}<VAR>c : Cardinal.{max u_2 u_3}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>#ι < c.ord.cof
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>φ : C(↑(σₙ R a), R)₀ →⋆ₙₐ[R] A<VAR>hφ₁ : Continuous ⇑φ<VAR>hφ₂ : φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a<GOAL>(cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ }
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>IsBlock G B ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>(∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>(∀ (g : G) (x : X), g⁻¹ • x ∈ B → x ∈ B → g • B = B) ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>⨆ i, LinearMap.range (ι Q) ^ i = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>iSup (evenOdd Q) = ⨆ i, LinearMap.range (ι Q) ^ i
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<VAR>ha : a ≠ 0<GOAL>a = a * b ↔ b = 1
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p j : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>F : ℕ → ℚ<VAR>S : Finset ℕ<VAR>hS : S.Nonempty<VAR>hF : ∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)<VAR>hn1 : ∀ (i : ℕ), 0 < F i<GOAL>padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p j : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>F : ℕ → ℚ<VAR>S : Finset ℕ<VAR>hn1 : ∀ (i : ℕ), 0 < F i<VAR>k : ℕ<VAR>hF : ∀ i ∈ {k}, padicValRat p (F j) < padicValRat p (F i)<GOAL>padicValRat p (F j) < padicValRat p (∑ i ∈ {k}, F i)