ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite<VAR>C' : ℝ<VAR>hC' : ∀ i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'<VAR>this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'<GOAL>∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite<VAR>C' : ℝ<VAR>hC' : ∀ i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'<VAR>this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'<VAR>x : α<VAR>h₀ : g'' x ≠ 0<GOAL>‖f x‖ ≤ max C C' * ‖g'' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : f =O[cofinite] g''<VAR>C : ℝ<VAR>C₀ : C > 0<VAR>hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite<VAR>C' : ℝ<VAR>hC' : ∀ i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'<VAR>this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'<VAR>x : α<VAR>h₀ : g'' x ≠ 0<GOAL>C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S T : Set E<GOAL>restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r₁ r₂ : ℝ<GOAL>⟪r₁ • (o.rotation ↑(π / 2)) x, r₂ • x⟫_ℝ = 0
<VAR>m n✝ : ℕ<VAR>k : Fin (n✝ + 1 + 1)<GOAL>k ≤ k - 1 ↔ k = 0
<VAR>m n✝ : ℕ<VAR>k : Fin (n✝ + 1 + 1)<GOAL>↑k ≤ ↑(k - 1) ↔ k = 0
<VAR>m n✝ : ℕ<VAR>k : Fin (n✝ + 1 + 1)<GOAL>k = k + 1 → k = 0
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Module A M<VAR>κ : Type u_6<VAR>inst✝² : Fintype κ<VAR>ι' : Type u_7<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>tb : Trunc (Basis ι A M)<VAR>b' : Basis ι' A M<VAR>f : M →ₗ[A] M<GOAL>(detAux tb) f = ((toMatrix b' b') f).det
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>i : ι<GOAL>MeasurableSet {ω | (fun ω => min (τ ω) (π ω)) ω ≤ i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>i : ι<GOAL>MeasurableSet ({a | τ a ≤ i} ∪ {a | π a ≤ i})
<VAR>ι : Type u_1<VAR>F : Filter ι<VAR>f : ι → ℝ<VAR>h : Bornology.IsBounded (range f)<GOAL>IsBounded (fun x x_1 => x ≤ x_1) (map f F)
<VAR>ι : Type u_1<VAR>F : Filter ι<VAR>f : ι → ℝ<VAR>h : Bornology.IsBounded (range f)<VAR>c : ℝ<VAR>hc : c ∈ upperBounds (range f)<GOAL>IsBounded (fun x x_1 => x ≤ x_1) (map f F)
<VAR>J : Type u'<VAR>inst✝¹ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ PresheafedSpace C<VAR>j : J<VAR>U : (Opens ↑↑(F.obj j))ᵒᵖ<GOAL>(F.map (𝟙 j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom.app U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<GOAL>𝓝[{a}] a = pure a
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪r • (o.rotation ↑(π / 2)) x, x⟫_ℝ = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ≥0∞<GOAL>⇑h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>A : Type u_2<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : IsScalarTower R A M<VAR>N : Type u_4<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module A N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsScalarTower R A N<VAR>r : R<VAR>m : M<GOAL>r • m = (algebraMap R A) r • m
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>y ∈ ball x ε ↔ edist x y < ε
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * (λ ^ (3 * S.multiplicity - 5) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * FermatLastTheoremForThreeGen.Solution.X S ^ 3)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)<GOAL>↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 = λ ^ 2 * (λ ^ (3 * S.multiplicity - 5) * ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * FermatLastTheoremForThreeGen.Solution.X S ^ 3)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<GOAL>↑b ^ (clog b r - 1) < r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<GOAL>r⁻¹ < ↑b ^ (log b r⁻¹ + 1)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<GOAL>0 < ↑b ^ (log b r⁻¹ + 1)
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : ⋯.IsPrimitiveClassified<GOAL>h.IsClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : ⋯.IsPrimitiveClassified<GOAL>↑(x.gcd y) ∣ x
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : ⋯.IsPrimitiveClassified<GOAL>↑(x.gcd y) ∣ y
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : ⋯.IsPrimitiveClassified<GOAL>↑(x.gcd y) ∣ z
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hfμ : Integrable f μ<VAR>h_int : Integrable (llr μ ν) μ<VAR>hfν : Integrable (fun x => rexp (f x)) ν<GOAL>Integrable (llr μ (ν.tilted f)) μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hfμ : Integrable f μ<VAR>h_int : Integrable (llr μ ν) μ<VAR>hfν : Integrable (fun x => rexp (f x)) ν<GOAL>Integrable (fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>H K : Subgroup G<GOAL>map f H ≤ map f K ↔ H ≤ K ⊔ f.ker
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop atTop<VAR>r : ℝ<VAR>hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a<VAR>i : ℕ<VAR>hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a<VAR>hi' : ∀ (a : ℕ), f a < r + 1 → a < i<GOAL>{a | r < f a}ᶜ ⊆ {a | a ≤ i}
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop atTop<VAR>r : ℝ<VAR>hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a<VAR>i : ℕ<VAR>hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a<VAR>hi' : ∀ (a : ℕ), f a < r + 1 → a < i<GOAL>{a | f a ≤ r} ⊆ {a | a ≤ i}
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : σ<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(rTensor (X s ⊗ₜ[R] n)) d = if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>a b c✝ d e : α<VAR>m n : ℤ<VAR>β : Type u_4<VAR>inst✝ : Preorder β<VAR>f : β → α<VAR>hf : StrictMono f<VAR>c : α<VAR>hc : 0 < c<GOAL>StrictMono fun x => f x / c
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : Finite α<VAR>hpα : p ∣ Nat.card α<VAR>a : α<VAR>ha : a ∈ fixedPoints G α<GOAL>∃ b ∈ fixedPoints G α, a ≠ b
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : Finite α<VAR>hpα : p ∣ Nat.card α<VAR>a : α<VAR>ha : a ∈ fixedPoints G α<VAR>hpf : p ∣ Nat.card ↑(fixedPoints G α)<GOAL>∃ b ∈ fixedPoints G α, a ≠ b
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : Finite α<VAR>hpα : p ∣ Nat.card α<VAR>a : α<VAR>ha : a ∈ fixedPoints G α<VAR>hpf : p ∣ Nat.card ↑(fixedPoints G α)<VAR>hα : 1 < Nat.card ↑(fixedPoints G α)<GOAL>∃ b ∈ fixedPoints G α, a ≠ b
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : Finite α<VAR>hpα : p ∣ Nat.card α<VAR>a : α<VAR>ha : a ∈ fixedPoints G α<VAR>hpf : p ∣ Nat.card ↑(fixedPoints G α)<VAR>hα : Nontrivial ↑(fixedPoints G α)<GOAL>∃ b ∈ fixedPoints G α, a ≠ b
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A✝ B C A X Y : Rep k G<VAR>f : X ⟶ Y<VAR>g : ↑(MonCat.of G)<VAR>x : ↑((fun B => of (A.ρ.linHom B.ρ)) X).V<VAR>y : CoeSort.coe A<GOAL>f.hom ((X.ρ g) ((x ∘ₗ A.ρ g⁻¹) y)) = ((ModuleCat.ofHom ((LinearMap.llcomp k (CoeSort.coe A) (CoeSort.coe X) (CoeSort.coe Y)) f.hom) ≫ ((fun B => of (A.ρ.linHom B.ρ)) Y).ρ g) x) y
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A✝ B C A X Y : Rep k G<VAR>f : X ⟶ Y<VAR>g : ↑(MonCat.of G)<VAR>x : ↑((fun B => of (A.ρ.linHom B.ρ)) X).V<VAR>y : CoeSort.coe A<GOAL>(Y.ρ g) (f.hom ((x ∘ₗ A.ρ g⁻¹) y)) = ((ModuleCat.ofHom ((LinearMap.llcomp k (CoeSort.coe A) (CoeSort.coe X) (CoeSort.coe Y)) f.hom) ≫ (of (A.ρ.linHom Y.ρ)).ρ g) x) y
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : Preorder γ<VAR>inst✝ : Preorder δ<VAR>u : γ → α<VAR>v : δ → β<VAR>hu : CauchySeq u<VAR>hv : CauchySeq v<GOAL>CauchySeq (Prod.map u v)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>m n : ℕ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℤ<GOAL>A⁻¹ ^ n = A ^ (-n)
<VAR>m n k : ℕ<GOAL>(n * k + m).Coprime n ↔ m.Coprime n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t✝ : Set α<VAR>s : Finset α<VAR>f : α → Filter β<VAR>t : Set β<GOAL>t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t✝ : Set α<VAR>s : Finset α<VAR>f : α → Filter β<VAR>t : Set β<GOAL>t ∈ ⨅ x, f ↑x ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s t : SignedMeasure α<GOAL>{ re := ↑s ∅, im := ↑t ∅ } = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s t : SignedMeasure α<GOAL>{ re := 0, im := 0 } = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s t : SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>{ re := ↑s i, im := ↑t i } = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s t : SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasurableSet i<GOAL>{ re := 0, im := 0 } = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>p.support ∆ q.support ⊆ (p + q).support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>p.support \ q.support ⊆ (p + q).support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>q.support \ p.support ⊆ (p + q).support
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>ι : Type u_2<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommGroup (G i)<VAR>inst✝² : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>i : ι<VAR>g : G i<VAR>m : M<GOAL>(toDirectLimit f M) ((of R ι G f i) g ⊗ₜ[R] m) = (of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>ι : Type u_2<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommGroup (G i)<VAR>inst✝² : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>i : ι<VAR>g : G i<VAR>m : M<GOAL>(((mk R (G i) M).compr₂ (of R ι (fun _i => G _i ⊗[R] M) (fun _i _j h => LinearMap.rTensor M (f _i _j h)) i)) g) m = (of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
<VAR>α✝² : Type u_1<VAR>α✝¹ : Type u_2<VAR>α✝ : Type u_3<VAR>f : α✝² → α✝¹ → α✝<VAR>l : List α✝²<VAR>l' : List α✝¹<GOAL>(zipWith f l l').tail = zipWith f l.tail l'.tail
<VAR>α✝² : Type u_1<VAR>α✝¹ : Type u_2<VAR>α✝ : Type u_3<VAR>f : α✝² → α✝¹ → α✝<VAR>l : List α✝²<VAR>l' : List α✝¹<GOAL>drop 1 (zipWith f l l') = zipWith f l.tail l'.tail
<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>comm : Commute g h<VAR>x : α<GOAL>x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C b * X ^ 2 + C c * X + C d).degree < (C a * X ^ 3).degree
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>IsLocalAtTarget (stalkwise fun {R S} [CommRing R] [CommRing S] => P)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso<GOAL>IsLocalAtTarget (stalkwise fun {R S} [CommRing R] [CommRing S] => P)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso<VAR>this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP<GOAL>IsLocalAtTarget (stalkwise fun {R S} [CommRing R] [CommRing S] => P)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso<VAR>this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP<GOAL>∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f → stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ U)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso<VAR>this : (stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso := stalkwise_respectsIso hP<GOAL>∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ U i)) → stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f
<VAR>α : Type u_1<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : 0 < a<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : 0 < a<GOAL>(fun x => 1) =ᶠ[nhds a] ⇑SignType.sign
<VAR>α : Type u_1<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : 0 < a<GOAL>∃ t, (∀ y ∈ t, 1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t
<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝ : T2Space M<GOAL>tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝ : T2Space M<GOAL>closure (↑(extChartAt I c).symm '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)) ⊆ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : (p.append q).IsPath<GOAL>q.IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : (p.append q).reverse.IsPath<GOAL>q.reverse.IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : (q.reverse.append p.reverse).IsPath<GOAL>q.reverse.IsPath
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c : γ<VAR>f : α → γ → γ<VAR>a : α<VAR>h : ∀ (b : γ), f a b = b<VAR>t : Finset γ<GOAL>↑(image₂ f {a} t) = ↑t
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.14175, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ a₃ : A<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : B<VAR>h₁ : b₁ = φ a₁<VAR>h₂ : b₂ = φ a₂<VAR>h₃ : b₃ = φ a₃<GOAL>b₁ + b₂ = b₃